Library Equations.Equations

The set of libraries required to run Equations with all features.

From Equations Require Export Loader.
From Equations Require Import Telescopes.

Tactic to solve well-founded proof obligations by default

Ltac solve_rec := simpl in * ; cbv zeta ; intros ;
try typeclasses eauto with subterm_relation Below rec_decision.