> defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1) is a theorem. (proof) Sure. My point is just that a theorem is a proposition equipped with a proo

> defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1) is a theorem. (proof) Sure. My point is just that a theorem is a proposition equipped with a proof. If the user just enters a proposition into the system, then they aren't entering a theorem. They're entering a proposition that the system can turn into a theorem.