# HG changeset patch
# User lcp
# Date 776968289 -7200
# Node ID 35c70ab82940169c0b22df1c642cf7852f3abd99
# Parent  85d7ff169b9cb191dd00e9527fca18ea51aeb144
ZF/ex/CoUnit/lleq_cs: copied from LList.ML

diff -r 85d7ff169b9c -r 35c70ab82940 src/ZF/ex/CoUnit.ML
--- a/src/ZF/ex/CoUnit.ML	Mon Aug 15 18:27:50 1994 +0200
+++ b/src/ZF/ex/CoUnit.ML	Mon Aug 15 18:31:29 1994 +0200
@@ -58,6 +58,9 @@
 by (etac counit2.elim 1);
 by (etac counit2.elim 1);
 by (rewrite_goals_tac counit2.con_defs);
+val lleq_cs = subset_cs
+	addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
+        addSEs [Ord_in_Ord, Pair_inject];
 by (fast_tac lleq_cs 1);
 val counit2_Int_Vset_subset_lemma = result();