let res := match! term with
                           | context[?v]
                             => lazy_match! v with
                                | @type.try_transport ?base_type ?try_make_transport_base_type_cps ?p ?t ?t
                                  => Some (v, p, t)
                                end
                           | _ => None
                           end in
                match res with
                | Some v
                  => let (v, p, t) := v in
                     let some_pt := debug_Constr_check (fun () => mkApp some [ mkApp p [t] ]) in
                     let term := lazy_match! (eval pattern v in term) with
                                 | ?term _ => term
                                 end in
                     let (term, args) := aux term in
                     (term, some_pt :: args)
                | None => (term, [])
                end