proposition: Lemma backward_consts: sigma • fst (constEQ x) ≡ sigma • snd (constEQ x) -> n = 1.
proof: Proof. Proof using Ex. cbn. unfold funcomp; change shift with (add 1); rewrite ren_plus_combine; unfold var_zero; cbn. rewrite Ex. asimpl. intros ? % equiv_lam_elim % equiv_lam_elim. eapply enc_injective;[| |eauto]; (eauto 2). Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)