proposition: Lemma last_string'_g : last_string' = g t.
proof: Proof. unfold g, c. ded (split_correct h2). rewrite H. ded (matches_correct h3). subst. refl. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(Srs LogicUtil SLoop ListUtil NatUtil RelUtil)