Documentation

d_Ren_4 ∷ Integer → Integer → () Source #

d_lift_14 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → T_Fin_10 → T_Fin_10 Source #

du_lift_14 ∷ (T_Fin_10 → T_Fin_10) → T_Fin_10 → T_Fin_10 Source #

d_renList_26 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → [T__'8866'_14] → [T__'8866'_14] Source #

d_ren_32 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → T__'8866'_14 → T__'8866'_14 Source #

d_weaken_88 ∷ Integer → T__'8866'_14 → T__'8866'_14 Source #

d_lift'45'cong_104 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T__'8801'__12) → T_Fin_10 → T__'8801'__12 Source #

d_renList'45'cong_124 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T__'8801'__12) → [T__'8866'_14] → T__'8801'__12 Source #

d_ren'45'cong_138 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T__'8801'__12) → T__'8866'_14 → T__'8801'__12 Source #

d_lift'45'id_196 ∷ Integer → T_Fin_10 → T__'8801'__12 Source #

d_lift'45'comp_212 ∷ Integer → Integer → Integer → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T_Fin_10) → T_Fin_10 → T__'8801'__12 Source #

d_renList'45'id_228 ∷ Integer → [T__'8866'_14] → T__'8801'__12 Source #

d_ren'45'id_234 ∷ Integer → T__'8866'_14 → T__'8801'__12 Source #

d_renList'45'comp_276 ∷ Integer → Integer → Integer → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T_Fin_10) → [T__'8866'_14] → T__'8801'__12 Source #

d_ren'45'comp_290 ∷ Integer → Integer → Integer → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T_Fin_10) → T__'8866'_14 → T__'8801'__12 Source #

d_Sub_368 ∷ Integer → Integer → () Source #

d_lifts_378 ∷ Integer → Integer → (T_Fin_10 → T__'8866'_14) → T_Fin_10 → T__'8866'_14 Source #

du_lifts_378 ∷ Integer → (T_Fin_10 → T__'8866'_14) → T_Fin_10 → T__'8866'_14 Source #

d_subList_390 ∷ Integer → Integer → (T_Fin_10 → T__'8866'_14) → [T__'8866'_14] → [T__'8866'_14] Source #

d_sub_396 ∷ Integer → Integer → (T_Fin_10 → T__'8866'_14) → T__'8866'_14 → T__'8866'_14 Source #

d_extend_454 ∷ Integer → Integer → (T_Fin_10 → T__'8866'_14) → T__'8866'_14 → T_Fin_10 → T__'8866'_14 Source #

du_extend_454 ∷ (T_Fin_10 → T__'8866'_14) → T__'8866'_14 → T_Fin_10 → T__'8866'_14 Source #

d__'91'_'93'_468 ∷ Integer → T__'8866'_14 → T__'8866'_14 → T__'8866'_14 Source #

d_lifts'45'cong_486 ∷ Integer → Integer → (T_Fin_10 → T__'8866'_14) → (T_Fin_10 → T__'8866'_14) → (T_Fin_10 → T__'8801'__12) → T_Fin_10 → T__'8801'__12 Source #

d_subList'45'cong_506 ∷ Integer → Integer → (T_Fin_10 → T__'8866'_14) → (T_Fin_10 → T__'8866'_14) → (T_Fin_10 → T__'8801'__12) → [T__'8866'_14] → T__'8801'__12 Source #

d_sub'45'cong_520 ∷ Integer → Integer → (T_Fin_10 → T__'8866'_14) → (T_Fin_10 → T__'8866'_14) → (T_Fin_10 → T__'8801'__12) → T__'8866'_14 → T__'8801'__12 Source #

d_lifts'45'id_578 ∷ Integer → T_Fin_10 → T__'8801'__12 Source #

d_subList'45'id_586 ∷ Integer → [T__'8866'_14] → T__'8801'__12 Source #

d_sub'45'id_592 ∷ Integer → T__'8866'_14 → T__'8801'__12 Source #

d_lifts'45'lift_634 ∷ Integer → Integer → Integer → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T__'8866'_14) → T_Fin_10 → T__'8801'__12 Source #

d_subList'45'ren_658 ∷ Integer → Integer → Integer → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T__'8866'_14) → [T__'8866'_14] → T__'8801'__12 Source #

d_sub'45'ren_672 ∷ Integer → Integer → Integer → (T_Fin_10 → T_Fin_10) → (T_Fin_10 → T__'8866'_14) → T__'8866'_14 → T__'8801'__12 Source #

d_ren'45'lift'45'lifts_762 ∷ Integer → Integer → Integer → (T_Fin_10 → T__'8866'_14) → (T_Fin_10 → T_Fin_10) → T_Fin_10 → T__'8801'__12 Source #

d_renList'45'sub_786 ∷ Integer → Integer → Integer → (T_Fin_10 → T__'8866'_14) → (T_Fin_10 → T_Fin_10) → [T__'8866'_14] → T__'8801'__12 Source #

d_ren'45'sub_800 ∷ Integer → Integer → Integer → (T_Fin_10 → T__'8866'_14) → (T_Fin_10 → T_Fin_10) → T__'8866'_14 → T__'8801'__12 Source #

d_lifts'45'comp_890 ∷ Integer → Integer → Integer → (T_Fin_10 → T__'8866'_14) → (T_Fin_10 → T__'8866'_14) → T_Fin_10 → T__'8801'__12 Source #

d_subList'45'comp_914 ∷ Integer → Integer → Integer → (T_Fin_10 → T__'8866'_14) → (T_Fin_10 → T__'8866'_14) → [T__'8866'_14] → T__'8801'__12 Source #

d_sub'45'comp_928 ∷ Integer → Integer → Integer → (T_Fin_10 → T__'8866'_14) → (T_Fin_10 → T__'8866'_14) → T__'8866'_14 → T__'8801'__12 Source #