Documentation

d_Ren_4 :: Integer -> Integer -> () #

d_lift_14 :: Integer -> Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10 #

du_lift_14 :: (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10 #

d_renList_26 :: Integer -> Integer -> (T_Fin_10 -> T_Fin_10) -> [T__'8866'_14] -> [T__'8866'_14] #

d_ren_32 :: Integer -> Integer -> (T_Fin_10 -> T_Fin_10) -> T__'8866'_14 -> T__'8866'_14 #

d_weaken_88 :: Integer -> T__'8866'_14 -> T__'8866'_14 #

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 #

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 #

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 #

d_lift'45'id_196 :: Integer -> T_Fin_10 -> T__'8801'__12 #

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 #

d_renList'45'id_228 :: Integer -> [T__'8866'_14] -> T__'8801'__12 #

d_ren'45'id_234 :: Integer -> T__'8866'_14 -> T__'8801'__12 #

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 #

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 #

d_Sub_368 :: Integer -> Integer -> () #

d_lifts_378 :: Integer -> Integer -> (T_Fin_10 -> T__'8866'_14) -> T_Fin_10 -> T__'8866'_14 #

du_lifts_378 :: Integer -> (T_Fin_10 -> T__'8866'_14) -> T_Fin_10 -> T__'8866'_14 #

d_subList_390 :: Integer -> Integer -> (T_Fin_10 -> T__'8866'_14) -> [T__'8866'_14] -> [T__'8866'_14] #

d_sub_396 :: Integer -> Integer -> (T_Fin_10 -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14 #

d_extend_454 :: Integer -> Integer -> (T_Fin_10 -> T__'8866'_14) -> T__'8866'_14 -> T_Fin_10 -> T__'8866'_14 #

du_extend_454 :: (T_Fin_10 -> T__'8866'_14) -> T__'8866'_14 -> T_Fin_10 -> T__'8866'_14 #

d__'8593''738'_470 :: Integer -> Integer -> (T_Fin_10 -> T__'8866'_14) -> T_Fin_10 -> T__'8866'_14 #

du__'8593''738'_470 :: Integer -> (T_Fin_10 -> T__'8866'_14) -> T_Fin_10 -> T__'8866'_14 #

d__'91'_'93'_478 :: Integer -> T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14 #

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 #

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 #

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 #

d_lifts'45'id_588 :: Integer -> T_Fin_10 -> T__'8801'__12 #

d_subList'45'id_596 :: Integer -> [T__'8866'_14] -> T__'8801'__12 #

d_sub'45'id_602 :: Integer -> T__'8866'_14 -> T__'8801'__12 #

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 #

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 #

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 #

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 #

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 #

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 #

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 #

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 #

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 #