proposition: Lemma AbsR_EnsembleOfList_FiniteSetOfListOfFiniteSetAndListOfList ls : AbsR (projT2 FiniteSetImpl) (EnsembleOfList ls) (FiniteSetOfList (snd (FiniteSetAndListOfList ls))).
proof: Proof. induction ls; simpl. { handle_calls_then' ltac:(fun H => idtac). inversion_by computes_to_inv; subst; trivial. } { handle_calls_then' ltac:(fun H => rewrite NoListJustFiniteSetOfList in *; specialize (H _ (AbsR_EnsembleOfList_FiniteSetOfList _))). inversion_by computes_to_inv. destruct_head_hnf prod; destruct_head_hnf bool; t. { unfold EnsembleOfList in *; simpl in *. rewrite NoFunctionJustFiniteSetOfFunction in *. handle_calls_then' ltac:(fun H => specialize (H _ (AbsR_EnsembleOfList_FiniteSetOfList _))). t. eauto. } { unfold EnsembleOfList in *; simpl in *. rewrite NoFunctionJustFiniteSetOfFunction in *. let th := handle_calls_then' ltac:(fun H => match goal with | [ H' : AbsR _ _ _ |- _ ] => specialize (H _ H') | _ => specialize (H _ (AbsR_EnsembleOfList_FiniteSetOfList _)) end) in th; inversion_by computes_to_inv; t; eauto; th; inversion_by computes_to_inv; t; eauto; th; inversion_by computes_to_inv; t. } } Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.RelationPairs Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTRefinement.Core Fiat.ADTNotation Fiat.ADTRefinement.GeneralRefinements Fiat.Computation Fiat.Common Fiat.Common.Ensembles Fiat.Common.Ensembles.Tactics Fiat.ComputationalEnsembles Fiat.FiniteSetADTs.FiniteSetADTMethodLaws Fiat.FiniteSetADTs.FiniteSetADT