------------------------------------------------------------------------
-- The Agda standard library
--
-- Helpers intended to ease the development of "tactics" which use
-- proof by reflection
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Data.Fin.Base using (Fin)
open import Data.Nat.Base using (ℕ)
open import Data.Vec.Base as Vec using (Vec; allFin)
open import Function.Base using (id)
open import Function.Bundles using (module Equivalence)
open import Level using (Level)
open import Relation.Binary.Bundles using (Setoid)

-- Think of the parameters as follows:
--
-- * Expr:    A representation of code.
-- * var:     The Expr type should support a notion of variables.
-- * ⟦_⟧:     Computes the semantics of an expression. Takes an
--            environment mapping variables to something.
-- * ⟦_⇓⟧:    Computes the semantics of the normal form of the
--            expression.
-- * correct: Normalisation preserves the semantics.
--
-- Given these parameters two "tactics" are returned, prove and solve.
--
-- For an example of the use of this module, see Algebra.RingSolver.

module Relation.Binary.Reflection
         {e a s}
         {Expr : ℕ → Set e} {A : Set a}
         (Sem : Setoid a s) (open Setoid Sem using (Carrier; _≈_))
         (var : ∀ {n} → Fin n → Expr n)
         (⟦_⟧ ⟦_⇓⟧ : ∀ {n} → Expr n → Vec A n → Carrier)
         (correct : ∀ {n} (e : Expr n) ρ → $\begin{pmatrix} \,\href{Relation.Binary.Reflection.html#1460}{\htmlId{1478}{\htmlClass{Bound}{\text{e}}}}\, \,\href{Relation.Binary.Reflection.html#1390}{\htmlId{1480}{\htmlClass{Bound Operator}{\text{⇓⟧}}}}\, \,\href{Relation.Binary.Reflection.html#1472}{\htmlId{1483}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Relation.Binary.Bundles.html#1293}{\htmlId{1485}{\htmlClass{Field Operator}{\text{≈}}}}\, \begin{pmatrix} \,\href{Relation.Binary.Reflection.html#1460}{\htmlId{1489}{\htmlClass{Bound}{\text{e}}}}\, \end{pmatrix} \,\href{Relation.Binary.Reflection.html#1472}{\htmlId{1493}{\htmlClass{Bound}{\text{ρ}}}}\,)
         \,\htmlId{1505}{\htmlClass{Keyword}{\text{where}}}\,

\,\htmlId{1512}{\htmlClass{Keyword}{\text{open}}}\, \,\htmlId{1517}{\htmlClass{Keyword}{\text{import}}}\, \,\href{Data.Vec.N-ary.html}{\htmlId{1524}{\htmlClass{Module}{\text{Data.Vec.N-ary}}}}\,
\,\htmlId{1539}{\htmlClass{Keyword}{\text{open}}}\, \,\htmlId{1544}{\htmlClass{Keyword}{\text{import}}}\, \,\href{Data.Product.Base.html}{\htmlId{1551}{\htmlClass{Module}{\text{Data.Product.Base}}}}\, \,\htmlId{1569}{\htmlClass{Keyword}{\text{using}}}\, (\,\href{Data.Product.Base.html#1618}{\htmlId{1576}{\htmlClass{Function Operator}{\text{\_×\_}}}}\,\,\htmlId{1579}{\htmlClass{Symbol}{\text{;}}}\, \,\href{Agda.Builtin.Sigma.html#235}{\htmlId{1581}{\htmlClass{InductiveConstructor Operator}{\text{\_,\_}}}}\,\,\htmlId{1584}{\htmlClass{Symbol}{\text{;}}}\, \,\href{Data.Product.Base.html#636}{\htmlId{1586}{\htmlClass{Field}{\text{proj₁}}}}\,\,\htmlId{1591}{\htmlClass{Symbol}{\text{;}}}\, \,\href{Data.Product.Base.html#650}{\htmlId{1593}{\htmlClass{Field}{\text{proj₂}}}}\,)
\,\htmlId{1600}{\htmlClass{Keyword}{\text{import}}}\, \,\href{Relation.Binary.PropositionalEquality.Core.html}{\htmlId{1607}{\htmlClass{Module}{\text{Relation.Binary.PropositionalEquality.Core}}}}\, \,\htmlId{1650}{\htmlClass{Symbol}{\text{as}}}\, \,\htmlId{1653}{\htmlClass{Module}{\text{≡}}}\,
\,\htmlId{1655}{\htmlClass{Keyword}{\text{import}}}\, \,\href{Relation.Binary.Reasoning.Setoid.html}{\htmlId{1662}{\htmlClass{Module}{\text{Relation.Binary.Reasoning.Setoid}}}}\, \,\htmlId{1695}{\htmlClass{Symbol}{\text{as}}}\, \,\htmlId{1698}{\htmlClass{Module}{\text{≈-Reasoning}}}\,

\,\htmlId{1711}{\htmlClass{Keyword}{\text{open}}}\, \,\href{Relation.Binary.Reasoning.Setoid.html}{\htmlId{1716}{\htmlClass{Module}{\text{≈-Reasoning}}}}\, \,\href{Relation.Binary.Reflection.html#1279}{\htmlId{1728}{\htmlClass{Bound}{\text{Sem}}}}\,

\,\htmlId{1733}{\htmlClass{Comment}{\text{-- If two normalised expressions are semantically equal, then their}}}\,
\,\htmlId{1801}{\htmlClass{Comment}{\text{-- non-normalised forms are also equal.}}}\,

\,\href{Relation.Binary.Reflection.html#1842}{\htmlId{1842}{\htmlClass{Function}{\text{prove}}}}\, \,\htmlId{1848}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{1850}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{1852}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Relation.Binary.Reflection.html#1853}{\htmlId{1853}{\htmlClass{Bound}{\text{n}}}}\,\,\htmlId{1854}{\htmlClass{Symbol}{\text{}}}}\, (\,\href{Relation.Binary.Reflection.html#1857}{\htmlId{1857}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{1859}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Data.Vec.Base.html#1119}{\htmlId{1861}{\htmlClass{Datatype}{\text{Vec}}}}\, \,\href{Relation.Binary.Reflection.html#1258}{\htmlId{1865}{\htmlClass{Bound}{\text{A}}}}\, \,\href{Relation.Binary.Reflection.html#1853}{\htmlId{1867}{\htmlClass{Bound}{\text{n}}}}\,) \,\href{Relation.Binary.Reflection.html#1870}{\htmlId{1870}{\htmlClass{Bound}{\text{e₁}}}}\, \,\href{Relation.Binary.Reflection.html#1873}{\htmlId{1873}{\htmlClass{Bound}{\text{e₂}}}}\, \,\htmlId{1876}{\htmlClass{Symbol}{\text{→}}}\,
        \begin{pmatrix} \,\href{Relation.Binary.Reflection.html#1870}{\htmlId{1888}{\htmlClass{Bound}{\text{e₁}}}}\, \,\href{Relation.Binary.Reflection.html#1390}{\htmlId{1891}{\htmlClass{Bound Operator}{\text{⇓⟧}}}}\, \,\href{Relation.Binary.Reflection.html#1857}{\htmlId{1894}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Relation.Binary.Bundles.html#1293}{\htmlId{1896}{\htmlClass{Field Operator}{\text{≈}}}}\, \begin{pmatrix} \,\href{Relation.Binary.Reflection.html#1873}{\htmlId{1900}{\htmlClass{Bound}{\text{e₂}}}}\, \,\href{Relation.Binary.Reflection.html#1390}{\htmlId{1903}{\htmlClass{Bound Operator}{\text{⇓⟧}}}}\, \,\href{Relation.Binary.Reflection.html#1857}{\htmlId{1906}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{1908}{\htmlClass{Symbol}{\text{→}}}\,
        \begin{pmatrix} \,\href{Relation.Binary.Reflection.html#1870}{\htmlId{1920}{\htmlClass{Bound}{\text{e₁}}}}\,  \end{pmatrix} \,\href{Relation.Binary.Reflection.html#1857}{\htmlId{1926}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Relation.Binary.Bundles.html#1293}{\htmlId{1928}{\htmlClass{Field Operator}{\text{≈}}}}\, \begin{pmatrix} \,\href{Relation.Binary.Reflection.html#1873}{\htmlId{1932}{\htmlClass{Bound}{\text{e₂}}}}\,  \end{pmatrix} \,\href{Relation.Binary.Reflection.html#1857}{\htmlId{1938}{\htmlClass{Bound}{\text{ρ}}}}\,
\,\href{Relation.Binary.Reflection.html#1842}{\htmlId{1940}{\htmlClass{Function}{\text{prove}}}}\, \,\href{Relation.Binary.Reflection.html#1946}{\htmlId{1946}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Relation.Binary.Reflection.html#1948}{\htmlId{1948}{\htmlClass{Bound}{\text{e₁}}}}\, \,\href{Relation.Binary.Reflection.html#1951}{\htmlId{1951}{\htmlClass{Bound}{\text{e₂}}}}\, \,\href{Relation.Binary.Reflection.html#1954}{\htmlId{1954}{\htmlClass{Bound}{\text{hyp}}}}\, \,\htmlId{1958}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Binary.Reasoning.Syntax.html#1572}{\htmlId{1960}{\htmlClass{Function Operator}{\text{begin}}}}\,
  \begin{pmatrix} \,\href{Relation.Binary.Reflection.html#1948}{\htmlId{1970}{\htmlClass{Bound}{\text{e₁}}}}\,  \end{pmatrix} \,\href{Relation.Binary.Reflection.html#1946}{\htmlId{1976}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Relation.Binary.Reasoning.Syntax.html#7136}{\htmlId{1978}{\htmlClass{Function}{\text{≈⟨}}}}\, \,\href{Relation.Binary.Reflection.html#1443}{\htmlId{1981}{\htmlClass{Bound}{\text{correct}}}}\, \,\href{Relation.Binary.Reflection.html#1948}{\htmlId{1989}{\htmlClass{Bound}{\text{e₁}}}}\, \,\href{Relation.Binary.Reflection.html#1946}{\htmlId{1992}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Relation.Binary.Reasoning.Syntax.html#7136}{\htmlId{1994}{\htmlClass{Function}{\text{⟨}}}}\,
  \begin{pmatrix} \,\href{Relation.Binary.Reflection.html#1948}{\htmlId{2000}{\htmlClass{Bound}{\text{e₁}}}}\, \,\href{Relation.Binary.Reflection.html#1390}{\htmlId{2003}{\htmlClass{Bound Operator}{\text{⇓⟧}}}}\, \,\href{Relation.Binary.Reflection.html#1946}{\htmlId{2006}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Relation.Binary.Reasoning.Syntax.html#7111}{\htmlId{2008}{\htmlClass{Function}{\text{≈⟨}}}}\, \,\href{Relation.Binary.Reflection.html#1954}{\htmlId{2011}{\htmlClass{Bound}{\text{hyp}}}}\, \,\href{Relation.Binary.Reasoning.Syntax.html#7111}{\htmlId{2015}{\htmlClass{Function}{\text{⟩}}}}\,
  \begin{pmatrix} \,\href{Relation.Binary.Reflection.html#1951}{\htmlId{2021}{\htmlClass{Bound}{\text{e₂}}}}\, \,\href{Relation.Binary.Reflection.html#1390}{\htmlId{2024}{\htmlClass{Bound Operator}{\text{⇓⟧}}}}\, \,\href{Relation.Binary.Reflection.html#1946}{\htmlId{2027}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Relation.Binary.Reasoning.Syntax.html#7111}{\htmlId{2029}{\htmlClass{Function}{\text{≈⟨}}}}\, \,\href{Relation.Binary.Reflection.html#1443}{\htmlId{2032}{\htmlClass{Bound}{\text{correct}}}}\, \,\href{Relation.Binary.Reflection.html#1951}{\htmlId{2040}{\htmlClass{Bound}{\text{e₂}}}}\, \,\href{Relation.Binary.Reflection.html#1946}{\htmlId{2043}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Relation.Binary.Reasoning.Syntax.html#7111}{\htmlId{2045}{\htmlClass{Function}{\text{⟩}}}}\,
  \begin{pmatrix} \,\href{Relation.Binary.Reflection.html#1951}{\htmlId{2051}{\htmlClass{Bound}{\text{e₂}}}}\,  \end{pmatrix} \,\href{Relation.Binary.Reflection.html#1946}{\htmlId{2057}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Relation.Binary.Reasoning.Syntax.html#12345}{\htmlId{2059}{\htmlClass{Function Operator}{\text{∎}}}}\,

\,\htmlId{2062}{\htmlClass{Comment}{\text{-- Applies the function to all possible "variables".}}}\,

\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{2116}{\htmlClass{Function}{\text{close}}}}\, \,\htmlId{2122}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{2124}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{2126}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Relation.Binary.Reflection.html#2127}{\htmlId{2127}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{2129}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Primitive.html#388}{\htmlId{2131}{\htmlClass{Primitive}{\text{Set}}}}\, \,\href{Relation.Binary.Reflection.html#1222}{\htmlId{2135}{\htmlClass{Bound}{\text{e}}}}\,\,\htmlId{2136}{\htmlClass{Symbol}{\text{}}}}\, \,\href{Relation.Binary.Reflection.html#2138}{\htmlId{2138}{\htmlClass{Bound}{\text{n}}}}\, \,\htmlId{2140}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Data.Vec.N-ary.html#1168}{\htmlId{2142}{\htmlClass{Function}{\text{N-ary}}}}\, \,\href{Relation.Binary.Reflection.html#2138}{\htmlId{2148}{\htmlClass{Bound}{\text{n}}}}\, (\,\href{Relation.Binary.Reflection.html#1239}{\htmlId{2151}{\htmlClass{Bound}{\text{Expr}}}}\, \,\href{Relation.Binary.Reflection.html#2138}{\htmlId{2156}{\htmlClass{Bound}{\text{n}}}}\,) \,\href{Relation.Binary.Reflection.html#2127}{\htmlId{2159}{\htmlClass{Bound}{\text{A}}}}\, \,\htmlId{2161}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Relation.Binary.Reflection.html#2127}{\htmlId{2163}{\htmlClass{Bound}{\text{A}}}}\,
\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{2165}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#2171}{\htmlId{2171}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#2173}{\htmlId{2173}{\htmlClass{Bound}{\text{f}}}}\, \,\htmlId{2175}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Binary.Reflection.html#2173}{\htmlId{2177}{\htmlClass{Bound}{\text{f}}}}\, \,\href{Data.Vec.N-ary.html#1516}{\htmlId{2179}{\htmlClass{Function Operator}{\text{$ⁿ}}}}\, \,\href{Data.Vec.Base.html#2955}{\htmlId{2182}{\htmlClass{Function}{\text{Vec.map}}}}\, \,\href{Relation.Binary.Reflection.html#1346}{\htmlId{2190}{\htmlClass{Bound}{\text{var}}}}\, (\,\href{Data.Vec.Base.html#6708}{\htmlId{2195}{\htmlClass{Function}{\text{allFin}}}}\, \,\href{Relation.Binary.Reflection.html#2171}{\htmlId{2202}{\htmlClass{Bound}{\text{n}}}}\,)

\,\htmlId{2206}{\htmlClass{Comment}{\text{-- A variant of prove which should in many cases be easier to use,}}}\,
\,\htmlId{2273}{\htmlClass{Comment}{\text{-- because variables and environments are handled in a less explicit}}}\,
\,\htmlId{2342}{\htmlClass{Comment}{\text{-- way.}}}\,
\,\htmlId{2350}{\htmlClass{Comment}{\text{--}}}\,
\,\htmlId{2353}{\htmlClass{Comment}{\text{-- If the type signature of solve is a bit daunting, then it may be}}}\,
\,\htmlId{2421}{\htmlClass{Comment}{\text{-- helpful to instantiate n with a small natural number and normalise}}}\,
\,\htmlId{2491}{\htmlClass{Comment}{\text{-- the remainder of the type.}}}\,

\,\href{Relation.Binary.Reflection.html#2522}{\htmlId{2522}{\htmlClass{Function}{\text{solve}}}}\, \,\htmlId{2528}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{2530}{\htmlClass{Symbol}{\text{∀}}}\, \,\href{Relation.Binary.Reflection.html#2532}{\htmlId{2532}{\htmlClass{Bound}{\text{n}}}}\, (\,\href{Relation.Binary.Reflection.html#2535}{\htmlId{2535}{\htmlClass{Bound}{\text{f}}}}\, \,\htmlId{2537}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Data.Vec.N-ary.html#1168}{\htmlId{2539}{\htmlClass{Function}{\text{N-ary}}}}\, \,\href{Relation.Binary.Reflection.html#2532}{\htmlId{2545}{\htmlClass{Bound}{\text{n}}}}\, (\,\href{Relation.Binary.Reflection.html#1239}{\htmlId{2548}{\htmlClass{Bound}{\text{Expr}}}}\, \,\href{Relation.Binary.Reflection.html#2532}{\htmlId{2553}{\htmlClass{Bound}{\text{n}}}}\,) (\,\href{Relation.Binary.Reflection.html#1239}{\htmlId{2557}{\htmlClass{Bound}{\text{Expr}}}}\, \,\href{Relation.Binary.Reflection.html#2532}{\htmlId{2562}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Data.Product.Base.html#1618}{\htmlId{2564}{\htmlClass{Function Operator}{\text{×}}}}\, \,\href{Relation.Binary.Reflection.html#1239}{\htmlId{2566}{\htmlClass{Bound}{\text{Expr}}}}\, \,\href{Relation.Binary.Reflection.html#2532}{\htmlId{2571}{\htmlClass{Bound}{\text{n}}}}\,) \,\htmlId{2575}{\htmlClass{Symbol}{\text{→}}}\,
  \,\href{Data.Vec.N-ary.html#2526}{\htmlId{2579}{\htmlClass{Function}{\text{Eqʰ}}}}\, \,\href{Relation.Binary.Reflection.html#2532}{\htmlId{2583}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Bundles.html#1293}{\htmlId{2585}{\htmlClass{Field Operator}{\text{\_≈\_}}}}\, (\,\href{Data.Vec.N-ary.html#1379}{\htmlId{2590}{\htmlClass{Function}{\text{curryⁿ}}}}\, \begin{pmatrix} \,\href{Data.Product.Base.html#636}{\htmlId{2599}{\htmlClass{Field}{\text{proj₁}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{2606}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#2532}{\htmlId{2612}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#2535}{\htmlId{2614}{\htmlClass{Bound}{\text{f}}}}\,) \,\href{Relation.Binary.Reflection.html#1390}{\htmlId{2617}{\htmlClass{Bound Operator}{\text{⇓⟧}}}}\,) (\,\href{Data.Vec.N-ary.html#1379}{\htmlId{2622}{\htmlClass{Function}{\text{curryⁿ}}}}\, \begin{pmatrix} \,\href{Data.Product.Base.html#650}{\htmlId{2631}{\htmlClass{Field}{\text{proj₂}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{2638}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#2532}{\htmlId{2644}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#2535}{\htmlId{2646}{\htmlClass{Bound}{\text{f}}}}\,) \,\href{Relation.Binary.Reflection.html#1390}{\htmlId{2649}{\htmlClass{Bound Operator}{\text{⇓⟧}}}}\,) \,\htmlId{2653}{\htmlClass{Symbol}{\text{→}}}\,
  \,\href{Data.Vec.N-ary.html#2282}{\htmlId{2657}{\htmlClass{Function}{\text{Eq}}}}\,  \,\href{Relation.Binary.Reflection.html#2532}{\htmlId{2661}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Bundles.html#1293}{\htmlId{2663}{\htmlClass{Field Operator}{\text{\_≈\_}}}}\, (\,\href{Data.Vec.N-ary.html#1379}{\htmlId{2668}{\htmlClass{Function}{\text{curryⁿ}}}}\, \begin{pmatrix} \,\href{Data.Product.Base.html#636}{\htmlId{2677}{\htmlClass{Field}{\text{proj₁}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{2684}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#2532}{\htmlId{2690}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#2535}{\htmlId{2692}{\htmlClass{Bound}{\text{f}}}}\,)  \end{pmatrix}) (\,\href{Data.Vec.N-ary.html#1379}{\htmlId{2700}{\htmlClass{Function}{\text{curryⁿ}}}}\, \begin{pmatrix} \,\href{Data.Product.Base.html#650}{\htmlId{2709}{\htmlClass{Field}{\text{proj₂}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{2716}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#2532}{\htmlId{2722}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#2535}{\htmlId{2724}{\htmlClass{Bound}{\text{f}}}}\,)  \end{pmatrix})
\,\href{Relation.Binary.Reflection.html#2522}{\htmlId{2731}{\htmlClass{Function}{\text{solve}}}}\, \,\href{Relation.Binary.Reflection.html#2737}{\htmlId{2737}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#2739}{\htmlId{2739}{\htmlClass{Bound}{\text{f}}}}\, \,\href{Relation.Binary.Reflection.html#2741}{\htmlId{2741}{\htmlClass{Bound}{\text{hyp}}}}\, \,\htmlId{2745}{\htmlClass{Symbol}{\text{=}}}\,
  \,\href{Data.Vec.N-ary.html#4270}{\htmlId{2749}{\htmlClass{Function}{\text{curryⁿ-cong}}}}\, \,\href{Relation.Binary.Bundles.html#1293}{\htmlId{2761}{\htmlClass{Field Operator}{\text{\_≈\_}}}}\, \begin{pmatrix} \,\href{Data.Product.Base.html#636}{\htmlId{2767}{\htmlClass{Field}{\text{proj₁}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{2774}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#2737}{\htmlId{2780}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#2739}{\htmlId{2782}{\htmlClass{Bound}{\text{f}}}}\,) \end{pmatrix} \begin{pmatrix} \,\href{Data.Product.Base.html#650}{\htmlId{2789}{\htmlClass{Field}{\text{proj₂}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{2796}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#2737}{\htmlId{2802}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#2739}{\htmlId{2804}{\htmlClass{Bound}{\text{f}}}}\,) \end{pmatrix}
    ( \,\href{Relation.Binary.Reflection.html#2816}{\htmlId{2816}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2818}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Relation.Binary.Reflection.html#1842}{\htmlId{2820}{\htmlClass{Function}{\text{prove}}}}\, \,\href{Relation.Binary.Reflection.html#2816}{\htmlId{2826}{\htmlClass{Bound}{\text{ρ}}}}\, (\,\href{Data.Product.Base.html#636}{\htmlId{2829}{\htmlClass{Field}{\text{proj₁}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{2836}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#2737}{\htmlId{2842}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#2739}{\htmlId{2844}{\htmlClass{Bound}{\text{f}}}}\,) (\,\href{Data.Product.Base.html#650}{\htmlId{2849}{\htmlClass{Field}{\text{proj₂}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{2856}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#2737}{\htmlId{2862}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#2739}{\htmlId{2864}{\htmlClass{Bound}{\text{f}}}}\,)
             (\,\href{Data.Vec.N-ary.html#4564}{\htmlId{2882}{\htmlClass{Function}{\text{curryⁿ-cong⁻¹}}}}\, \,\href{Relation.Binary.Bundles.html#1293}{\htmlId{2896}{\htmlClass{Field Operator}{\text{\_≈\_}}}}\,
                \begin{pmatrix} \,\href{Data.Product.Base.html#636}{\htmlId{2918}{\htmlClass{Field}{\text{proj₁}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{2925}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#2737}{\htmlId{2931}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#2739}{\htmlId{2933}{\htmlClass{Bound}{\text{f}}}}\,) \,\href{Relation.Binary.Reflection.html#1390}{\htmlId{2936}{\htmlClass{Bound Operator}{\text{⇓⟧}}}}\, \begin{pmatrix} \,\href{Data.Product.Base.html#650}{\htmlId{2941}{\htmlClass{Field}{\text{proj₂}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{2948}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#2737}{\htmlId{2954}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#2739}{\htmlId{2956}{\htmlClass{Bound}{\text{f}}}}\,) \,\href{Relation.Binary.Reflection.html#1390}{\htmlId{2959}{\htmlClass{Bound Operator}{\text{⇓⟧}}}}\,
                (\,\href{Data.Vec.N-ary.html#5589}{\htmlId{2979}{\htmlClass{Function}{\text{Eqʰ-to-Eq}}}}\, \,\href{Relation.Binary.Reflection.html#2737}{\htmlId{2989}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Bundles.html#1293}{\htmlId{2991}{\htmlClass{Field Operator}{\text{\_≈\_}}}}\, \,\href{Relation.Binary.Reflection.html#2741}{\htmlId{2995}{\htmlClass{Bound}{\text{hyp}}}}\,) \,\href{Relation.Binary.Reflection.html#2816}{\htmlId{3000}{\htmlClass{Bound}{\text{ρ}}}}\,)

\,\htmlId{3005}{\htmlClass{Comment}{\text{-- A variant of solve which does not require that the normal form}}}\,
\,\htmlId{3071}{\htmlClass{Comment}{\text{-- equality is proved for an arbitrary environment.}}}\,

\,\href{Relation.Binary.Reflection.html#3124}{\htmlId{3124}{\htmlClass{Function}{\text{solve₁}}}}\, \,\htmlId{3131}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{3133}{\htmlClass{Symbol}{\text{∀}}}\, \,\href{Relation.Binary.Reflection.html#3135}{\htmlId{3135}{\htmlClass{Bound}{\text{n}}}}\, (\,\href{Relation.Binary.Reflection.html#3138}{\htmlId{3138}{\htmlClass{Bound}{\text{f}}}}\, \,\htmlId{3140}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Data.Vec.N-ary.html#1168}{\htmlId{3142}{\htmlClass{Function}{\text{N-ary}}}}\, \,\href{Relation.Binary.Reflection.html#3135}{\htmlId{3148}{\htmlClass{Bound}{\text{n}}}}\, (\,\href{Relation.Binary.Reflection.html#1239}{\htmlId{3151}{\htmlClass{Bound}{\text{Expr}}}}\, \,\href{Relation.Binary.Reflection.html#3135}{\htmlId{3156}{\htmlClass{Bound}{\text{n}}}}\,) (\,\href{Relation.Binary.Reflection.html#1239}{\htmlId{3160}{\htmlClass{Bound}{\text{Expr}}}}\, \,\href{Relation.Binary.Reflection.html#3135}{\htmlId{3165}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Data.Product.Base.html#1618}{\htmlId{3167}{\htmlClass{Function Operator}{\text{×}}}}\, \,\href{Relation.Binary.Reflection.html#1239}{\htmlId{3169}{\htmlClass{Bound}{\text{Expr}}}}\, \,\href{Relation.Binary.Reflection.html#3135}{\htmlId{3174}{\htmlClass{Bound}{\text{n}}}}\,) \,\htmlId{3178}{\htmlClass{Symbol}{\text{→}}}\,
         \,\href{Data.Vec.N-ary.html#1751}{\htmlId{3189}{\htmlClass{Function}{\text{∀ⁿ}}}}\, \,\href{Relation.Binary.Reflection.html#3135}{\htmlId{3192}{\htmlClass{Bound}{\text{n}}}}\, (\,\href{Data.Vec.N-ary.html#1379}{\htmlId{3195}{\htmlClass{Function}{\text{curryⁿ}}}}\, \,\htmlId{3202}{\htmlClass{Symbol}{\text{λ}}}\, \,\href{Relation.Binary.Reflection.html#3204}{\htmlId{3204}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{3206}{\htmlClass{Symbol}{\text{→}}}\,
                 \begin{pmatrix} \,\href{Data.Product.Base.html#636}{\htmlId{3227}{\htmlClass{Field}{\text{proj₁}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3234}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#3135}{\htmlId{3240}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#3138}{\htmlId{3242}{\htmlClass{Bound}{\text{f}}}}\,) \,\href{Relation.Binary.Reflection.html#1390}{\htmlId{3245}{\htmlClass{Bound Operator}{\text{⇓⟧}}}}\, \,\href{Relation.Binary.Reflection.html#3204}{\htmlId{3248}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Relation.Binary.Bundles.html#1293}{\htmlId{3250}{\htmlClass{Field Operator}{\text{≈}}}}\, \begin{pmatrix} \,\href{Data.Product.Base.html#650}{\htmlId{3254}{\htmlClass{Field}{\text{proj₂}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3261}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#3135}{\htmlId{3267}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#3138}{\htmlId{3269}{\htmlClass{Bound}{\text{f}}}}\,) \,\href{Relation.Binary.Reflection.html#1390}{\htmlId{3272}{\htmlClass{Bound Operator}{\text{⇓⟧}}}}\, \,\href{Relation.Binary.Reflection.html#3204}{\htmlId{3275}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{3277}{\htmlClass{Symbol}{\text{→}}}\,
                 \begin{pmatrix} \,\href{Data.Product.Base.html#636}{\htmlId{3298}{\htmlClass{Field}{\text{proj₁}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3305}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#3135}{\htmlId{3311}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#3138}{\htmlId{3313}{\htmlClass{Bound}{\text{f}}}}\,)  \end{pmatrix} \,\href{Relation.Binary.Reflection.html#3204}{\htmlId{3319}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Relation.Binary.Bundles.html#1293}{\htmlId{3321}{\htmlClass{Field Operator}{\text{≈}}}}\, \begin{pmatrix} \,\href{Data.Product.Base.html#650}{\htmlId{3325}{\htmlClass{Field}{\text{proj₂}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3332}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#3135}{\htmlId{3338}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#3138}{\htmlId{3340}{\htmlClass{Bound}{\text{f}}}}\,)  \end{pmatrix} \,\href{Relation.Binary.Reflection.html#3204}{\htmlId{3346}{\htmlClass{Bound}{\text{ρ}}}}\,)
\,\href{Relation.Binary.Reflection.html#3124}{\htmlId{3349}{\htmlClass{Function}{\text{solve₁}}}}\, \,\href{Relation.Binary.Reflection.html#3356}{\htmlId{3356}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#3358}{\htmlId{3358}{\htmlClass{Bound}{\text{f}}}}\, \,\htmlId{3360}{\htmlClass{Symbol}{\text{=}}}\,
  \,\href{Function.Bundles.html#4834}{\htmlId{3364}{\htmlClass{Field}{\text{Equivalence.from}}}}\, (\,\href{Data.Vec.N-ary.html#3249}{\htmlId{3382}{\htmlClass{Function}{\text{uncurry-∀ⁿ}}}}\, \,\href{Relation.Binary.Reflection.html#3356}{\htmlId{3393}{\htmlClass{Bound}{\text{n}}}}\,) \,\htmlId{3396}{\htmlClass{Symbol}{\text{λ}}}\, \,\href{Relation.Binary.Reflection.html#3398}{\htmlId{3398}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{3400}{\htmlClass{Symbol}{\text{→}}}\,
    \,\href{Relation.Binary.PropositionalEquality.Core.html#1989}{\htmlId{3406}{\htmlClass{Function}{\text{≡.subst}}}}\, \,\href{Function.Base.html#704}{\htmlId{3414}{\htmlClass{Function}{\text{id}}}}\, (\,\href{Relation.Binary.PropositionalEquality.Core.html#1893}{\htmlId{3418}{\htmlClass{Function}{\text{≡.sym}}}}\, (\,\href{Data.Vec.N-ary.html#2850}{\htmlId{3425}{\htmlClass{Function}{\text{left-inverse}}}}\, ( \,\href{Relation.Binary.Reflection.html#3441}{\htmlId{3441}{\htmlClass{Bound}{\text{\_}}}}\, \,\htmlId{3443}{\htmlClass{Symbol}{\text{→}}}\, \,\htmlId{3445}{\htmlClass{Symbol}{\text{\_}}}\, \,\href{Relation.Binary.Bundles.html#1293}{\htmlId{3447}{\htmlClass{Field Operator}{\text{≈}}}}\, \,\htmlId{3449}{\htmlClass{Symbol}{\text{\_}}}\, \,\htmlId{3451}{\htmlClass{Symbol}{\text{→}}}\, \,\htmlId{3453}{\htmlClass{Symbol}{\text{\_}}}\, \,\href{Relation.Binary.Bundles.html#1293}{\htmlId{3455}{\htmlClass{Field Operator}{\text{≈}}}}\, \,\htmlId{3457}{\htmlClass{Symbol}{\text{\_)}}}\, \,\href{Relation.Binary.Reflection.html#3398}{\htmlId{3460}{\htmlClass{Bound}{\text{ρ}}}}\,)
      (\,\href{Relation.Binary.Reflection.html#1842}{\htmlId{3471}{\htmlClass{Function}{\text{prove}}}}\, \,\href{Relation.Binary.Reflection.html#3398}{\htmlId{3477}{\htmlClass{Bound}{\text{ρ}}}}\, (\,\href{Data.Product.Base.html#636}{\htmlId{3480}{\htmlClass{Field}{\text{proj₁}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3487}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#3356}{\htmlId{3493}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#3358}{\htmlId{3495}{\htmlClass{Bound}{\text{f}}}}\,) (\,\href{Data.Product.Base.html#650}{\htmlId{3500}{\htmlClass{Field}{\text{proj₂}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3507}{\htmlClass{Function}{\text{close}}}}\, \,\href{Relation.Binary.Reflection.html#3356}{\htmlId{3513}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Relation.Binary.Reflection.html#3358}{\htmlId{3515}{\htmlClass{Bound}{\text{f}}}}\,)

\,\htmlId{3521}{\htmlClass{Comment}{\text{-- A variant of \_,\_ which is intended to make uses of solve and solve₁}}}\,
\,\htmlId{3592}{\htmlClass{Comment}{\text{-- look a bit nicer.}}}\,

\,\htmlId{3614}{\htmlClass{Keyword}{\text{infix}}}\, \,\htmlId{3620}{\htmlClass{Number}{\text{4}}}\, \,\href{Relation.Binary.Reflection.html#3627}{\htmlId{3622}{\htmlClass{Function Operator}{\text{\_⊜\_}}}}\,

\,\href{Relation.Binary.Reflection.html#3627}{\htmlId{3627}{\htmlClass{Function Operator}{\text{\_⊜\_}}}}\, \,\htmlId{3631}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{3633}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{3635}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Relation.Binary.Reflection.html#3636}{\htmlId{3636}{\htmlClass{Bound}{\text{n}}}}\,\,\htmlId{3637}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{3639}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Relation.Binary.Reflection.html#1239}{\htmlId{3641}{\htmlClass{Bound}{\text{Expr}}}}\, \,\href{Relation.Binary.Reflection.html#3636}{\htmlId{3646}{\htmlClass{Bound}{\text{n}}}}\, \,\htmlId{3648}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Relation.Binary.Reflection.html#1239}{\htmlId{3650}{\htmlClass{Bound}{\text{Expr}}}}\, \,\href{Relation.Binary.Reflection.html#3636}{\htmlId{3655}{\htmlClass{Bound}{\text{n}}}}\, \,\htmlId{3657}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Relation.Binary.Reflection.html#1239}{\htmlId{3659}{\htmlClass{Bound}{\text{Expr}}}}\, \,\href{Relation.Binary.Reflection.html#3636}{\htmlId{3664}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Data.Product.Base.html#1618}{\htmlId{3666}{\htmlClass{Function Operator}{\text{×}}}}\, \,\href{Relation.Binary.Reflection.html#1239}{\htmlId{3668}{\htmlClass{Bound}{\text{Expr}}}}\, \,\href{Relation.Binary.Reflection.html#3636}{\htmlId{3673}{\htmlClass{Bound}{\text{n}}}}\,
\,\href{Relation.Binary.Reflection.html#3627}{\htmlId{3675}{\htmlClass{Function Operator}{\text{\_⊜\_}}}}\, \,\htmlId{3679}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Sigma.html#235}{\htmlId{3681}{\htmlClass{InductiveConstructor Operator}{\text{\_,\_}}}}\,