proposition: Lemma conseqs_combine sigma s1 s2 t1 t2: sigma • (lambda lambda s1) ≡ sigma • (lambda lambda t1) /\ sigma • (lambda lambda s2) ≡ sigma • (lambda lambda t2) <-> sigma • (lambda lambda g s1 s2) ≡ sigma • (lambda lambda g t1 t2).
proof: Proof. cbn; split. - intros [H1 H2]; do 2 (eapply equiv_lam_elim in H1; eapply equiv_lam_elim in H2). now rewrite H1, H2. - intros H1; do 2 eapply equiv_lam_elim in H1. Injection H1. Injection H. now rewrite H0, H2. Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)