proposition: Lemma sysExtend (T U : System) (f : Formula): Included _ T U -> SysPrf T f -> SysPrf U f.
proof: Proof. apply (sysExtend LNT). Qed.
imports: Coq(Arith Ensembles List) hydras.Ackermann(Languages folProof folProp folLogic3)