proposition: Remark In_betaFormula_subst_2_1 : forall (a b : Term) (v : nat), In v (freeVarF (substF (substF βR 2 a) 1 b)) -> In v (freeVarT a) \/ In v (freeVarT b) \/ In v (@freeVarT LNN (var 0)).
proof: Proof. intros a b v H. destruct (freeVarSubFormula3 _ _ _ _ _ H) as [H0 | H0]. - assert (H1: In v (freeVarF (substF βR 2 a))). { eapply in_remove. apply H0. } decompose sum (In_betaFormula_subst_2 _ _ H1); try tauto. destruct H3 as [H2 | H2]. elim (in_remove_neq _ _ _ _ _ H0). symmetry in |- *; assumption. elim H2. - tauto. Qed.
imports: Coq(Arith) hydras.Ackermann(extEqualNat subAll folProp subProp folReplace folLogic3 NN NNtheory primRec expressible) Coqprime(ChineseRem) Coq(Vector List Lia) hydras(ListExt cPair MoreDecidable) hydras(Compat815 ssrnat_extracts) Coq(Utf8)