proposition: Lemma lift_brelation_hetero_true {A B R defaultA defaultB x y} : @lift_brelation_hetero A B R defaultA defaultB x y <-> @lift_relation_hetero A B R defaultA defaultB x y.
proof: Proof. unfold lift_brelation_hetero, lift_relation_hetero. apply (lift_relation_gen_hetero_iff2 (Q1 := is_true) (Q2 := fun x => x)); try tauto; try reflexivity; apply andb_true_iff. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances