]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
nasty change in the lexer/parser:
[helm.git] / helm / software / matita / contribs / formal_topology / overlap / basic_pairs_to_o-basic_pairs.ma
index 9e85452d585eebbb7b558a0d0a521f000689364f..3e2fe8f354ee116ad0e851d568893eaa14182b2a 100644 (file)
@@ -126,7 +126,8 @@ theorem BP_to_OBP_faithful:
  apply e;
 qed.
 
-theorem BP_to_OBP_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BP_to_OBP S T g = f).
+theorem BP_to_OBP_full: 
+   ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BP_to_OBP S T g = f).
  intros; 
  cases (POW_full (concr S) (concr T) (Oconcr_rel ?? f)) (gc Hgc);
  cases (POW_full (form S) (form T) (Oform_rel ?? f)) (gf Hgf);