fact: Definition find_app (ctx f: program) : term := let (_, f) := f in let (Σ, t) := ctx in let (_, goal) := decompose_prod_assum [] t in match goal with | tApp hd args => if eq_const hd f then goal else find_cnst_in_args f (split_apps (map (fun t => snd (decompose_prod_assum [] t)) args)) | _ => tVar "error: the goal does not have an application" end.
imports: MetaCoq.Template(All) MetaCoq.Utils(bytestring) List