proposition: Lemma ADT_ind {sig} (adt : ADT sig) : forall (P : Ensemble (Rep adt)) (PC : forall cidx r, fromConstructor (Constructors adt cidx) r -> P r) (PM : forall midx r r', fromMethod' (Methods adt midx r) r' -> P r'), forall r : Rep adt, fromADT adt r -> P r.
proof: Proof. intros. induction H. eapply PC. exact H. eapply PM. exact H0. Qed.
imports: Fiat.ADT Fiat.ADTNotation Coq.Sets.Ensembles Coq.Lists.List Fiat.Common.IterateBoundedIndex