fact: Fixpoint ty_Prop (t : ty) : Prop := match t with | base => False | arr ts t' => (fix tys_Prop (ts : list ty) := match ts with | nil => True | t'' :: ts' => ty_Prop t'' /\ tys_Prop ts' end) ts /\ ty_Prop t' end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List