proposition: Lemma punctured_downward_strict_sub : forall a x:E, axioms a -> inc x (U a) -> strict_sub (punctured_downward_subset a x) (U a).
proof: Proof. ir. uhg; ee. uhg; uhg; ir. assert (inc x (punctured_downward_subset a x)). rw H1; am. ufi punctured_downward_subset H2; Ztac. uh H4; xd. uhg; ir. ufi punctured_downward_subset H1; Ztac. Qed.
imports: Arith order