proposition: Lemma axioms_extensionality : forall a b, axioms a -> axioms b -> source a = source b -> target a = target b -> (forall x, ob (osource a) x -> ntrans a x = ntrans b x) -> a = b.
proof: Proof. ir. assert (like a). nw. assert (like b). nw. uh H4; uh H5. wr H4; wr H5. rw H1. rw H2. uf create. up. app Function.create_extensionality. ir. wri H1 H7. ap H3. ap is_ob_ob. nw. am. Qed.
imports: Arith functor