\import Data.List \hiding (Sort)
\import Data.Maybe
\import Logic
\import Logic.Meta
\import Paths
\import Data.Fin
\import Logic.Rewriting.TRS.HRS

\meta impossible-lambda => \lam e => contradiction

\func unwrap-func {env : FSignature} {s : Sort} {context : List Sort} {mc : MetaContext Sort}
                  (T : Term env context s mc) : Maybe
    (\Sigma (f : env.symbol s) (\Pi (index : Index (env.domain f)) ->
        Term env (context ++ (f FSignature.!!domain index)) (f FSignature.!!sort index) mc)) \elim T
  | var index p => nothing
  | metavar m arguments1 => nothing
  | func f1 arguments1 => just (f1, arguments1)

\func sigma-set-equalizer {A : \Set} {B : A -> \Type} {a : A} {b b' : B a} (p : (a,b) = {\Sigma (x : A) (B x)} (a,b')) : b = b' =>
  pmap (transport B __ b) (prop-isProp idp (pmap __. p)) *> pmapd __. p