proposition: Lemma compose_axioms : forall (a b c : E) (f g : E1), axioms b c f -> axioms a b g -> axioms a c (fun x : E => f (g x)).
proof: Proof. ir. unfold axioms in |- *. ir. unfold axioms in H. unfold axioms in H0. au. Qed.
imports: set_theory