proposition: Lemma subst_enc k e u: σ p q • e = enc k u -> exists e', e = enc k e' /\ σ p q • e' = u.
proof: Proof. Proof using τ n. induction k in e |-*; cbn. - intros; eexists; (intuition auto). - intros. simplify in *. destruct e as [ [| [| []]] | | | e1 e3 ]; try discriminate. destruct e1 as [ [| [| []]] | | | e1 e2 ]; try discriminate. destruct e1 as [ [| [| []]] | [] | | ]; try discriminate. destruct e2 as [ [| [| []]] | [[]|] | | ]; try discriminate. simplify in H. injection H as H. destruct (IHk _ H) as [e']; (intuition idtac); subst. exists e'. simplify. easy. Qed.
imports: List Lia Program.Program Undecidability.HOU(std.std axioms) RelationClasses Morphisms Init.Wf Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.goldfarb.encoding) FinFun Coq.Arith.Wf_nat