proposition: Lemma inclusion_strong_axioms : forall a b : E, sub (U a) (U b) -> strong_axioms (inclusion a b).
proof: Proof. ir. unfold inclusion in |- *. ap create_strong_axioms. unfold property in |- *. unfold Transformation.axioms in |- *. ir. ap H; au. Qed.
imports: Arith functions