proposition: Lemma D01 T i : SysPrf _ T (~ forallH i (P (v#i)) -> exH i, (~ (P (v#i))))%fol.
proof: Proof. apply sysExtend with (Empty_set _). - red; destruct 1. - intros; apply D0. Qed.
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)