Adding GRealize to uni_step.

[helm.git] / matita / matita / lib / basics / relations.ma

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index 8b6a79be5deec90a9f7820287174045f277bb533..36b5fc2a35339c14a222eb19fad339b0a6bf26a1 100644 (file)
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -62,6 +62,11 @@ definition inv ≝ λA.λR:relation A.λa,b.R b a.
 definition subR ≝ λA.λR,S:relation A.(∀a,b. R a b → S a b).
 interpretation "relation inclusion" 'subseteq R S = (subR ? R S).
 
+lemma sub_reflexive : 
+  ∀T.∀R:relation T.R ⊆ R.
+#T #R #x //
+qed.
+
 lemma sub_comp_l:  ∀A.∀R,R1,R2:relation A.
   R1 ⊆ R2 → R1 ∘ R ⊆ R2 ∘ R.
 #A #R #R1 #R2 #Hsub #a #b * #c * /4/