proposition: Lemma iffP_iff : forall x y, iffP x y <-> (Q x <-> Q y).
proof: Proof. intros [] []; compute; intuition congruence. Qed.
imports: Fiat.Common.FMapExtensions Fiat.Common.LogicFacts Fiat.Common.LogicMorphisms Fiat.Common