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(LogicUtil ATrs ListUtil RelUtil AMatching ListDec APosition NatUtil)