proposition: Lemma extens : forall a b : E, strong_axioms a -> strong_axioms b -> source a = source b -> target a = target b -> (forall x : E, inc x (U (source a)) -> inc x (U (source b)) -> ev a x = ev b x) -> a = b.
proof: Proof. ir. unfold strong_axioms in H, H0. xe. unfold like in H5, H4. rewrite <- H5. ap realizes_like_eq; au. unfold realizes in |- *. xe. ir. sy; ap H3. am. rewrite <- H1. am. Qed.
imports: Arith functions