(* *)
(**************************************************************************)
+include "ground_2/xoa/ex_1_2.ma".
+include "ground_2/xoa/ex_4_3.ma".
include "ground_2/relocation/rtmap_coafter.ma".
include "static_2/notation/relations/rdropstar_3.ma".
include "static_2/notation/relations/rdropstar_4.ma".
definition co_dropable_dx: predicate (rtmap → relation lenv) ≝
λR. ∀f2,L1,L2. R f2 L1 L2 →
∀b,f,K2. ⇩*[b,f] L2 ≘ K2 → 𝐔⦃f⦄ →
- ∀f1. f ~⊚ f1 ≘ f2 →
+ ∀f1. f ~⊚ f1 ≘ f2 →
∃∃K1. ⇩*[b,f] L1 ≘ K1 & R f1 K1 K2.
definition co_dedropable_sn: predicate (rtmap → relation lenv) ≝
lemma drops_isuni_ex: ∀f. 𝐔⦃f⦄ → ∀L. ∃K. ⇩*[Ⓕ,f] L ≘ K.
#f #H elim H -f /4 width=2 by drops_refl, drops_TF, ex_intro/
-#f #_ #g #H #IH destruct * /2 width=2 by ex_intro/
+#f #_ #g #H #IH destruct * /2 width=2 by ex_intro/
#L #I elim (IH L) -IH /3 width=2 by drops_drop, ex_intro/
qed-.