fact: Fixpoint fromConstructor {rep : Type} {dom : list Type} (const : constructorType rep dom) (r : rep) : Prop := match dom return constructorType rep dom -> rep -> Prop with | [ ] => fun const r => computes_to const r | D :: dom' => fun const r => exists (d : D), fromConstructor (const d) r end const r.
imports: Fiat.ADT Fiat.ADTNotation Coq.Sets.Ensembles Coq.Lists.List