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__'8593''738'_470 ∷ Integer → Integer → (T_Fin_10 → T__'8866'_14) → T_Fin_10 → T__'8866'_14 Source #

du__'8593''738'_470 ∷ Integer → (T_Fin_10 → T__'8866'_14) → T_Fin_10 → T__'8866'_14 Source #

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

d_lifts'45'cong_496 ∷ 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_516 ∷ 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_530 ∷ 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_588 ∷ Integer → T_Fin_10 → T__'8801'__12 Source #

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

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

d_lifts'45'lift_644 ∷ 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_668 ∷ 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_682 ∷ 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_772 ∷ 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_796 ∷ 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_810 ∷ 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_900 ∷ 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_924 ∷ 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_938 ∷ Integer → Integer → Integer → (T_Fin_10 → T__'8866'_14) → (T_Fin_10 → T__'8866'_14) → T__'8866'_14 → T__'8801'__12 Source #