- [ label_d n ⇒ l◗(path_head (m+n) q)
- | label_m ⇒ l◗(path_head m q)
- | label_L ⇒ l◗(path_head (↓o) q)
- | label_A ⇒ l◗(path_head m q)
- | label_S ⇒ l◗(path_head m q)
+ [ label_d k ⇒ (path_head (n+k) q)◖l
+ | label_m ⇒ (path_head n q)◖l
+ | label_L ⇒ (path_head (↓m) q)◖l
+ | label_A ⇒ (path_head n q)◖l
+ | label_S ⇒ (path_head n q)◖l
'DownArrowRight n p = (path_head n p).
(* basic constructions ****************************************************)
'DownArrowRight n p = (path_head n p).
(* basic constructions ****************************************************)
-[ #m <path_head_empty #H0
- <(eq_inv_empty_labels … H0) -m //
-| * [ #n ] #p #n @(nat_ind_succ … n) -n // #m #_
- [ <path_head_d_sn
- | <path_head_m_sn
- | <path_head_L_sn
- | <path_head_A_sn
- | <path_head_S_sn
+[ #n <path_head_empty #H0
+ <(eq_inv_empty_labels … H0) -n //
+| * [ #k ] #p #n @(nat_ind_succ … n) -n // #n #_
+ [ <path_head_d_dx
+ | <path_head_m_dx
+ | <path_head_L_dx
+ | <path_head_A_dx
+ | <path_head_S_dx
- | <path_head_d_sn <path_head_d_sn
- | <path_head_m_sn <path_head_m_sn
- | <path_head_L_sn <path_head_L_sn
- | <path_head_A_sn <path_head_A_sn
- | <path_head_S_sn <path_head_S_sn
+ | <path_head_d_dx <path_head_d_dx
+ | <path_head_m_dx <path_head_m_dx
+ | <path_head_L_dx <path_head_L_dx
+ | <path_head_A_dx <path_head_A_dx
+ | <path_head_S_dx <path_head_S_dx
- #n #_ cases l [ #m ]
- [ <path_head_d_sn <path_head_d_sn
- | <path_head_m_sn <path_head_m_sn
- | <path_head_L_sn <path_head_L_sn
- | <path_head_A_sn <path_head_A_sn
- | <path_head_S_sn <path_head_S_sn
+ #n #_ cases l [ #k ]
+ [ <path_head_d_dx <path_head_d_dx
+ | <path_head_m_dx <path_head_m_dx
+ | <path_head_L_dx <path_head_L_dx
+ | <path_head_A_dx <path_head_A_dx
+ | <path_head_S_dx <path_head_S_dx