proposition: Lemma foldeqs_correct sigma E: (forall s1 s2, (s1, s2) ∈ E -> (exists t, s1 = lambda lambda t) /\ (exists t, s2 = lambda lambda t)) -> (sigma •₊ left_side E) ≡₊ (sigma •₊ right_side E) <-> (sigma • fst (foldeqs E) ≡ sigma • snd (foldeqs E)).
proof: Proof. induction E as [| [s t]]; simplify. - cbn; firstorder. - intros H. apply id in H as H'. specialize (H' s t) as ([t1 H1]&[t2 H2]); lauto; subst. cbn. specialize (foldeqs_lambda_lambda E) as (u&v&H'); rewrite H' in *. mp IHE; (eauto 2). intros; eapply H; firstorder. cbn in IHE. cbn; unfold left_side, right_side in *. split; [intros [H1 H2] % equiv_lstep_cons_inv| intros H1]; do 2 eapply equiv_lam_elim in H1. + destruct IHE as [IHE _]; rewrite H1; mp IHE; (eauto 1); do 2 eapply equiv_lam_elim in IHE; now rewrite IHE. + Injection H1. Injection H0. rewrite H3. destruct IHE as [_ ->]; (eauto 2). now rewrite H2. Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)