proposition: Remark In_betaFormula_subst_1_2_0 : forall (a b c : Term) (v : nat), In v (freeVarF (substF3 βR 1 a 2 b 0 c)) -> In v (freeVarT a) \/ In v (freeVarT b) \/ In v (freeVarT c).
proof: Proof. intros a b c v H. destruct (freeVarSubFormula3 _ _ _ _ _ H) as [H0 | H0]. - assert (H1: In v (freeVarF (substF2 βR 1 a 2 b))). { eapply in_remove; apply H0. } destruct (freeVarSubFormula3 _ _ _ _ _ H1) as [H2 | H2]. + assert (H3: In v (freeVarF (substF βR 1 a))). { eapply in_remove; apply H2. } destruct (freeVarSubFormula3 _ _ _ _ _ H3) as [H4 | H4]. * destruct v as [| n]. -- elim (in_remove_neq _ _ _ _ _ H0). reflexivity. -- destruct n as [| n]. ++ elim (in_remove_neq _ _ _ _ _ H4); reflexivity. ++ destruct n as [| n]. ** elim (in_remove_neq _ _ _ _ _ H2). reflexivity. ** elim (proj1 (Nat.le_ngt (S (S (S n))) 2)). --- assert (H5: Representable 2 β βR). { apply betaRepresentable. } destruct H5 as (H5, H6). apply H5. eapply in_remove. exact H4. --- lia. * tauto. + tauto. - 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)