let prop_mk_iff = Prop.mk_iff