]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/dama/dama/ordered_set.ma
proof simplified
[helm.git] / helm / software / matita / contribs / dama / dama / ordered_set.ma
index b5b4d8e78beb6d10f471710baa79591d7532cffd..4c72cfd98d35dbbbc4c0f57134b6a88dc70b0866 100644 (file)
@@ -51,5 +51,3 @@ cases (os_cotransitive ??? a1 Eab) (H H); [cases (Laa1 H)]
 cases (os_cotransitive ??? b1 H) (H1 H1); [assumption]
 cases (Lb1b H1);
 qed.
-  
-  
\ No newline at end of file