+
+(* Basic properties *********************************************************)
+
+lemma simple_dec_ex (X): ∨∨ 𝐒❪X❫ | ∃∃p,I,T,U. X = ⓑ[p,I]T.U.
+* [ /2 width=1 by simple_atom, or_introl/ ]
+* [| /2 width=1 by simple_flat, or_introl/ ]
+/3 width=5 by ex1_4_intro, or_intror/
+qed-.