fact: Definition vars (Γ : env) (t : type) (g : G term) : G term := let vs := map (fun p => Id (snd p)) (filter (fun p => t = fst p?) (combine Γ (seq 0 (List.length Γ)))) in match vs with | [] => g | _ => oneOf_ (ret (Const 0)) [elems_ (Const 0) vs; g] end.
imports: mathcomp(ssreflect ssrbool eqtype) Arith List String Lia QuickChick(QuickChick)