I just pushed a fresh version of the
IndProp.v file I was going
through in class today that does not use
econstructor in the proofs I went over today. Use
apply for now
and will learn the constructor commands once you’re comfortable with
apply and inductive relations.