fact: Fixpoint find_cnst_in_args (f : term) (args : list term): term := match args with | nil => tVar "error: passed term does not appear in the goal" | cons a args => match a with | tApp hd a_args => if eq_const hd f then a else find_cnst_in_args f args | _ => find_cnst_in_args f args end end.
imports: MetaCoq.Template(All) MetaCoq.Utils(bytestring) List