proposition: Lemma enc_inv_motivation s: (forall x, x ∈ consts s -> R' x = None -> x ∈ C) -> inv_term C (enc_term C s) >* (fun x => AppR (var x) (map const C)) • s.
proof: Proof. Proof using n. intros H. replace (enc_term C s) with (var • enc_term C s) by now asimpl. rewrite enc_term_app; auto. Qed.
imports: List Arith Lia Morphisms Setoid Undecidability.HOU(calculus.calculus) Undecidability.HOU(unification.higher_order_unification unification.nth_order_unification concon.conservativity_constants concon.conservativity)