proposition: Lemma punctured_downward_for_ord : forall a x, next_compatible ID a -> inc x (U a) -> punctured_downward_subset a x = x.
proof: Proof. ir. util (ordinal_next (a:=a) (x:=x)). am. am. uh H. ee. ufi ID H2. ap H2. am. Qed.
imports: Arith transfinite