proposition: Lemma wf_Lt' : well_founded Lt'.
proof: Proof. intro. destruct a. destruct p. revert s. ded (wf_Lt e). elim H; clear H e; intros. apply Acc_intro. destruct y. destruct p. intro. apply H0. hyp. intro. apply Acc_intro. destruct y. destruct p; contr. contr. apply Acc_intro. destruct y. destruct p; contr. contr. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)