proposition: Theorem Conj : forall (Sini : S) (P1 P2 : S -> Prop), ForAll Sini P1 -> ForAll Sini P2 -> ForAll Sini (fun s : S => P1 s /\ P2 s).
proof: Proof. unfold ForAll in |- *; intros. split; [ apply H | apply H0 ]; assumption. Qed.
imports: time_clocks