proposition: Remark In_betaFormula_subst_2 : forall (a : Term) (v : nat), In v (freeVarF (substF βR 2 a)) -> In v (freeVarT a) \/ In v (@freeVarT LNN (var 1)) \/ In v (@freeVarT LNN (var 0)).
proof: Proof. intros a v H. rewrite <- (subFormulaId LNN βR 1) in H. decompose sum (In_betaFormula_subst_1_2 _ _ _ H); 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)