proposition: Theorem Mon_I : forall (Sini : S) (Pg Pp : S -> Prop), ForAll Sini Pg -> (forall s : S, Pg s -> Pp s) -> ForAll Sini Pp.
proof: Proof. unfold ForAll in |- *; intros. apply H0. apply H; assumption. Qed.
imports: time_clocks