Elpi Tactic rewrite.
(** Argument either the name of a hypothesis in the context,
    or the name of a global definition (variables count as global references
    as far as Elpi is concerned, although you can get a list of
    the section-local variables by calling coq.env.section.

    The declared type of the argument should be type is of the form
    [forall (x1 : A1) (x2 : A2) ... P = Q]

    Unifies Q with a subterm of the goal and rewrites right to left.
*)
Elpi Accumulate lp:{{
    pred nested_forall i:term, i:term, o:goal, o:list sealed-goal.
    nested_forall Eqpf {{@eq lp:S lp:P lp:Q }} (goal _ _ GoalType _ _ as G) GL :-
        pi x\ (copy J x :- coq.unify-leq Q J ok) =>
            copy GoalType (A x),
            if (occurs x (A x))
            (refine (match
                Eqpf
                (fun _ S (a\
                   fun _ {{ @eq lp:S lp:P lp:Q }} (_\ A a )
                   ))
                % We only want to create one hole,
                % the one corresponding to the
                % contents of the (single) branch of the match.
                [{{_}}])
                G GL
            )
            (coq.ltac.fail _ "Couldn't unify.").

    nested_forall Eqpf (prod _ A B) G GL :-
        Hole = {{ _ }},
        coq.typecheck Hole A ok,
        % This might not make progress if
        % Eqpf is opaque or an assumption.
        whd (app [Eqpf, Hole]) [] HD ARGS,
        unwind HD ARGS Eqpf',
        nested_forall Eqpf' (B Hole) G GL.

    solve (goal Ctx _ _ _ [trm Eq] as G) GL :- (
        % Eq is a direct reference to a global definition or axiom
        Eq = global Gref, coq.env.typeof Gref Ty;
        % Eq is a direct Gallina term and we will infer its type
        % from context
        coq.typecheck Eq Ty ok;
        % Eq is a reference to a declared variable in the context
        std.mem Ctx (decl Eq _ Ty)),
        nested_forall Eq Ty G GL.
}}.
Elpi Typecheck.