proposition: Lemma subst_t e k: σ p q • e = t k -> e = t k.
proof: Proof. unfold t; intros. destruct e as [ [| [| []]] | | | e1 e3 ] ; try discriminate. { cbn in *. asimpl in H. cbn in *. injection H as ?. destruct k; discriminate. } destruct e1 as [ [| [| []]] | | | e1 e2 ]; try discriminate. destruct e1 as [ [| [| []]] | [] | | ]; try discriminate. cbn -[add] in *. f_equal; injection H as H H'. asimpl in H. asimpl in H'. cbn in H, H'. unfold funcomp in H, H'. eapply subst_enc in H as [? []]; auto. eapply subst_enc in H' as [? []]; auto. subst. eapply subst_var_a in H0. eapply subst_var_b in H2. now subst. 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