proposition: Lemma le_subterm m n : m <= n -> (m = n \/ nat_subterm m n).
proof: Proof. induction 1. - left; reflexivity. - intuition subst. right; constructor. constructor. right. eapply Subterm.clos_trans_stepr; eauto. constructor. Qed.
imports: Program Equations.Prop.EqDecInstances Equations.Prop.Equations