proposition: Lemma decr_unifies sigma (s t: exp X) k: unifies sigma s t -> free' (free k) sigma -> unifies (decr k sigma) (Lambda k s) (Lambda k t).
proof: Proof. intros H1 [H2 H3]; unfold unifies in *; asimpl; f_equal. erewrite subst_extensional. symmetry. erewrite subst_extensional; eauto. all: intros x V; destruct (le_lt_dec k x). 1, 3: rewrite it_up_ge; eauto; unfold decr; asimpl. 1 - 2: rewrite Nat.sub_add; eauto; asimpl; rewrite subst_extensional with (tau := var); [now asimpl|]. 1 - 2: intros y ? % H3; unfold free in *; eauto; unfold funcomp; f_equal; lia. 1 - 2: rewrite it_up_lt; eauto; symmetry; eapply H2; unfold bound, free; lia. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)