proposition: Lemma decr_lambda_free k sigma: (forall x, lambda_free (sigma x)) -> (forall x, lambda_free (decr k sigma x)).
proof: Proof. intros H x; unfold decr; asimpl. eapply lambda_free_substitution; intros; cbn; eauto; econstructor. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)