fact: Fixpoint ExpressibleHelp (n : nat) : naryRel n -> Formula -> Prop := match n return (naryRel n -> Formula -> Prop) with | O => fun (R : naryRel 0) (A : Formula) => match R with | true => SysPrf T A | false => SysPrf T ( ~ A)%fol end | S m => fun (R : naryRel (S m)) (A : Formula) => forall a : nat, ExpressibleHelp m (R a) (substF A (S m) (natToTerm a)) end.
imports: Coq(Arith List) hydras.Ackermann(ListExt folProp subProp extEqualNat Languages LNN NewNotations)