Variable S : CSetoid.
Definition ⊆ (P Q : S -> CProp) : CProp := forall x : S, P x -> Q x.
Section Basics.
Variables P Q R : S -> CProp.
Lemma included_refl : ⊆ P P.
Lemma included_trans : ⊆ P Q -> ⊆ Q R -> ⊆ P R.
Lemma included_conj : forall P Q R, ⊆ P Q -> ⊆ P R -> ⊆ P (Conj Q R).
Lemma included_conj' : ⊆ (Conj P Q) P.
Lemma included_conj'' : ⊆ (Conj P Q) Q.
Lemma included_conj_lft : ⊆ R (Conj P Q) -> ⊆ R P.
Lemma included_conj_rht : ⊆ R (Conj P Q) -> ⊆ R Q.
Lemma included_extend : forall (H : forall x, P x -> CProp),
⊆ R (extend P H) -> ⊆ R P.
End Basics.
Let I,R:S->CProp and F G:(PartFunct S), and denote
by P and Q, respectively, the domains of F and G.
Variables F G : (PartFunct S).
Variable R : S -> CProp.
Lemma included_FComp : ⊆ R P -> (forall x Hx, (R x) -> Q (F x Hx)) -> ⊆ R (Dom (G[o]F)).
Lemma included_FComp' : ⊆ R (Dom (G[o]F)) -> ⊆ R P.
End inclusion.