proposition: Lemma leq_gen_mapping_unique : forall f g r s, is_leq_gen_mapping f g r -> is_leq_gen_mapping f g s -> domain r = domain s -> r = s.
proof: Proof. ir. ap extensionality. apply leq_gen_mapping_sub with f g; try am. rw H1; uhg; ir; am. apply leq_gen_mapping_sub with f g; try am; rw H1; uhg; ir; am. Qed.
imports: Arith order