proposition: Remark projRepresentable : forall (n m : nat) (pr : m < n), Representable n (evalProjFunc n m pr) (projFormula m).
proof: Proof. intros n m pr; unfold Representable in |- *. split. - simpl. lia. - induction n as [| n Hrecn]; try lia. simpl in |- *. intros a. destruct (Nat.eq_dec m n) as [e | e]. + rewrite e. clear e Hrecn pr m. induction n as [| n Hrecn]. * simpl in |- *. unfold projFormula in |- *. rewrite (subFormulaEqual LNN). apply iffRefl. * simpl in |- *. intros a0. unfold projFormula in |- *. repeat rewrite (subFormulaEqual LNN). simpl in |- *. destruct (Nat.eq_dec n n); try lia. replace (equal (var 0) (substT (n2t a) (S n) (n2t a0))) with (substF (v#0 = v#(n.+1))%fol (S n) (n2t a)). -- auto. -- rewrite subFormulaEqual; simpl in |- *. destruct (Nat.eq_dec n n); try lia. rewrite subTermNil; try reflexivity. apply closedNatToTerm. + apply RepresentableAlternate with (v#0 = v#(m.+1))%fol. * apply iffSym, subFormulaNil; simpl; lia. * auto. 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)