proposition: Remark In_betaFormula : forall v : nat, In v (freeVarF βR) -> In v (@freeVarT LNN (var 1)) \/ In v (@freeVarT LNN (var 2)) \/ In v (@freeVarT LNN (var 0)).
proof: Proof. intros v H. apply In_betaFormula_subst_1. rewrite (subFormulaId LNN). exact H. 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)