fact: Definition lift_relation_gen_hetero_Proper_Equal_impl := @lift_relation_gen_hetero_Proper_Equal_impl P Q and True HTrue Hand.
imports: Fiat.Common.FMapExtensions Fiat.Common.LogicFacts Fiat.Common.LogicMorphisms Fiat.Common