proposition: Lemma lift_relation_gen_hetero_iff {A B P} and True' (Q : P -> Prop) R defaultA defaultB (m1 : t A) (m2 : t B) (QTrue_or_key : Q True' \/ exists k, find k m1 = None /\ find k m2 = None) (Qand : forall x y, Q (and x y) <-> Q x /\ Q y) : Q (lift_relation_gen_hetero and True' R defaultA defaultB m1 m2) <-> forall k, Q (match find k m1, find k m2 with | Some x1, Some x2 => R x1 x2 | Some x, None => R x defaultB | None, Some x => R defaultA x | None, None => True' end).
proof: Proof. unfold lift_relation_gen_hetero. FMap_convert_to_find. rewrite fold_right_push_iff, fold_right_and_iff by (eassumption || exact _). FMap_convert_to_find. rewrite (forall_In_map Q); FMap_convert_to_find. split; [ intros [H QTrue'] k; specialize (fun P => H (k, P)) | intro H; split; [ intros [k ?]; specialize (H k) | destruct QTrue_or_key as [?| [k [? ?] ] ]; [ | specialize (H k) ] ] ]; simpl in *; break_match; repeat intuition (congruence || eauto || destruct_head' ex); instance_t. 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