proposition: Lemma of_list_elements {T} (v : t T) : Equal (of_list (elements v)) v.
proof: Proof. unfold of_list, Equal; intro y. destruct (find y v) eqn:H; FMap_convert; revert H; generalize (elements_3w v); induction (elements v) as [|x xs IHxs]; clear v. { simpl; intros; invlist InA. } { intros; invlist InA; invlist NoDupA; simpl in *; specialize_by assumption; FMap_convert_to_find; edestruct F.eq_dec; setoid_subst_E_eq; simpl in *; intuition (subst; setoid_subst_E_eq; eauto using (@reflexivity _ E.eq)). { exfalso; eauto using (@reflexivity _ E.eq). } { exfalso; destruct_head prod; eauto using InA_eqke_eqk. } } { simpl; intros; invlist InA. FMap_convert_to_find. intro; destruct_head ex; congruence. } { intros; invlist InA; invlist NoDupA; simpl in *; FMap_convert_to_find; edestruct F.eq_dec; setoid_subst_E_eq; simpl in *; intuition (subst; setoid_subst_E_eq; eauto using (@reflexivity _ E.eq)); destruct_head prod; repeat match goal with | [ H : (ex _) -> _ |- _ ] => specialize (fun x pf => H (ex_intro _ x pf)) | [ H : ((ex _) -> _) -> _ |- _ ] => specialize (fun f => H (fun xpf => match xpf with ex_intro x pf => f x pf end)) | [ H : ?A -> ?B -> ?C, H' : ?B |- _ ] => specialize (fun pf => H pf H') | _ => progress simpl in * end; eauto using (@reflexivity _ (@eq_key_elt T)), InA_cons_hd. } 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