proposition: Lemma last_term'_g : last_term' = g t.
proof: Proof. unfold g, c. destruct (subterm_pos_elim h2). destruct a. rewrite H0. ded (matches_correct h3). subst u. refl. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(ATrs LogicUtil ALoop ListUtil RelUtil NatUtil APosition AMatching ARelation)