proposition: Lemma freeVarPrimRecSigmaFormulaHelp1 : forall (n : nat) (A B : Formula) (v : nat), In v (freeVarF (primRecSigmaFormulaHelp n A B)) -> In v (freeVarF A) \/ In v (freeVarF B) \/ v = n.+2 \/ v = n.+1.
proof: Proof. intros n A B v H. unfold primRecSigmaFormulaHelp in H. assert (H0: forall v : nat, In v (freeVarF βR) -> v = 0 \/ v = 1 \/ v = 2). { intros v0 H0. assert (H1: Representable 2 β βR). apply betaRepresentable. destruct H1 as (H1, H2). apply H1 in H0. lia. } repeat match goal with | H:(In v (freeVarF (existH ?X1 ?X2))) |- _ => assert (In v (freeVarF X2)); [ eapply in_remove; apply H | assert (v <> X1); [ eapply in_remove_neq; apply H | clear H ] ] | H:(In v (freeVarF (forallH ?X1 ?X2))) |- _ => assert (In v (freeVarF X2)); [ eapply in_remove; apply H | assert (v <> X1); [ eapply in_remove_neq; apply H | clear H ] ] | H:(In v (List.remove _ ?X1 (freeVarF ?X2))) |- _ => assert (In v (freeVarF X2)); [ eapply in_remove; apply H | assert (v <> X1); [ eapply in_remove_neq; apply H | clear H ] ] | H:(In v (freeVarF (andH ?X1 ?X2))) |- _ => assert (In v (freeVarF X1 ++ freeVarF X2)); [ apply H | clear H ] | H:(In v (freeVarF (impH ?X1 ?X2))) |- _ => assert (In v (freeVarF X1 ++ freeVarF X2)); [ apply H | clear H ] | H:(In v (_ ++ _)) |- _ => destruct (in_app_or _ _ _ H); clear H | H:(In v (freeVarF (substF ?X1 ?X2 ?X3))) |- _ => induction (freeVarSubFormula3 _ _ _ _ _ H); clear H | H:(In v (freeVarF (LT ?X1 ?X2))) |- _ => rewrite freeVarLT in H | H:(In v (freeVarF βR)) |- _ => decompose sum (H0 v H); clear H end; try tauto; match goal with | H:(In v _) |- _ => simpl in H; decompose sum H; clear H end; auto; try match goal with | H:(?X1 = ?X2),H2:(?X2 <> ?X1) |- _ => elim H2; auto end; simpl in |- *; try 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)