Idris2Doc : Data.Telescope.Congruence

Data.Telescope.Congruence

N-ary congruence for reasoning
cong : (context : Fun () deltasy) -> congTypedelta () sycontext () sycontext
congSegment : (0 delta : Segmentngamma) -> (0 env1 : Environmentgamma) -> (0 sy1 : SimpleFunenv1deltaType) -> (0 lhs : Funenv1deltasy1) -> (0 env2 : Environmentgamma) -> (0 sy2 : SimpleFunenv2deltaType) -> (0 rhs : Funenv2deltasy2) -> (0 _ : env1 = env2) -> (0 _ : sy1 = sy2) -> (0 _ : lhs = rhs) -> congTypedeltaenv1sy1lhsenv2sy2rhs
congType : (delta : Segmentngamma) -> (env1 : Environmentgamma) -> (sy1 : SimpleFunenv1deltaType) -> Funenv1deltasy1 -> (env2 : Environmentgamma) -> (sy2 : SimpleFunenv2deltaType) -> Funenv2deltasy2 -> Type