proposition: Lemma sysExtend (T U : System) (f : Formula): Included _ T U -> SysPrf T f -> SysPrf U f.
proof: Proof. intros H [x [p H0]]; exists x, p. intros g H1; apply H, H0, H1. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)