+ 'ArrowEq u1 u2 = (subset_eq ? u1 u2).
+
+(* Basic destructions *******************************************************)
+
+lemma subset_in_eq_repl_back (A) (a:A):
+ âu1. a Ï” u1 â âu2. u1 â u2 â a Ï” u2.
+#A #a #u1 #Hu1 #u2 *
+/2 width=1 by/
+qed-.
+
+lemma subset_in_eq_repl_fwd (A) (a:A):
+ âu1. a Ï” u1 â âu2. u2 â u1 â a Ï” u2.
+#A #a #u1 #Hu1 #u2 *
+/2 width=1 by/
+qed-.