proposition: Lemma AbsR_EnsembleOfList_FiniteSetOfList ls : AbsR (projT2 FiniteSetImpl) (EnsembleOfList ls) (FiniteSetOfList ls).
proof: Proof. induction ls; simpl; handle_calls_then' ltac:(fun H => try specialize (H _ IHls)); pre_t; unfold EnsembleOfList in *; simpl; rewrite NoFunctionJustFiniteSetOfFunction; handle_calls_then' ltac:(fun H => try specialize (H _ IHls)); pre_t. { specialize_all_ways; auto. } { specialize_all_ways; auto. } { handle_calls_then' ltac:(fun H => try specialize (H _ IHls)); pre_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