fact: Definition decopt_has_type (Gamma : string -> option ty) (t : tm) (T : ty) (n : nat) : option bool := bindop (type_of Gamma t) (fun T' => Some ((T = T')?)).
imports: QuickChick(QuickChick) Coq(Nat) Coq(Arith.Arith) Coq(Logic.FunctionalExtensionality)