proposition: Lemma foldeqs_lambda_lambda E: exists s t, foldeqs E = (lambda lambda s, lambda lambda t).
proof: Proof. induction E as [|[s t]]; cbn; (eauto 2). - do 2 eexists; reflexivity. - destruct IHE as (s'&t'&IH). do 2 (destruct s; try solve [do 2 eexists; reflexivity]). do 2 (destruct t; try solve [do 2 eexists; reflexivity]). rewrite IH; do 2 eexists; reflexivity. Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)