proposition: Lemma backward_add: sigma • fst (addEQ x y z) ≡ sigma • snd (addEQ x y z) -> m + n = p.
proof: Proof. Proof using Ex Ey Ez. cbn. unfold funcomp; change shift with (add 1); rewrite !ren_plus_combine; unfold var_zero; cbn. rewrite Ex, Ey, Ez; simplify; intros H % equiv_lam_elim % equiv_lam_elim. rewrite <-enc_app in H. eapply enc_injective;[| |eauto]; (eauto 2). Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)