+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/grammar/lenv_append.ma".
-include "basic_2/relocation/ldrop.ma".
-
-(* DROPPING *****************************************************************)
-
-(* Properties on append for local environments ******************************)
-
-fact ldrop_O1_append_sn_le_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 →
- d = 0 → e ≤ |L1| →
- ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2.
-#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e normalize
-[2,3,4: /4 width=1 by ldrop_skip_lt, ldrop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ]
-#d #e #_ #_ #H <(le_n_O_to_eq … H) -H //
-qed-.
-
-lemma ldrop_O1_append_sn_le: ∀L1,L2,s,e. ⇩[s, 0, e] L1 ≡ L2 → e ≤ |L1| →
- ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2.
-/2 width=3 by ldrop_O1_append_sn_le_aux/ qed.
-
-(* Inversion lemmas on append for local environments ************************)
-
-lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K →
- |L2| ≤ e → ⇩[s, 0, e - |L2|] L1 ≡ K.
-#K #L1 #L2 elim L2 -L2 normalize //
-#L2 #I #V #IHL2 #s #e #H #H1e
-elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HL12 destruct
-[ lapply (le_n_O_to_eq … H1e) -H1e -IHL2
- >commutative_plus normalize #H destruct
-| <minus_plus >minus_minus_comm /3 width=1 by monotonic_pred/
-]
-qed-.
-
-lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → e ≤ |L2| →
- ∀K2. ⇩[s, 0, e] L2 ≡ K2 → K = L1 @@ K2.
-#K #L1 #L2 elim L2 -L2 normalize
-[ #s #e #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2
- #H2 elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct
- >(ldrop_inv_O2 … H1) -H1 //
-| #L2 #I #V #IHL2 #s #e @(nat_ind_plus … e) -e [ -IHL2 ]
- [ #H1 #_ #K2 #H2
- lapply (ldrop_inv_O2 … H1) -H1 #H1
- lapply (ldrop_inv_O2 … H2) -H2 #H2 destruct //
- | /4 width=7 by ldrop_inv_drop1, le_plus_to_le_r/
- ]
-]
-qed-.
--- /dev/null
+lemma length_inv_pos_dx_append: ∀d,L. |L| = d + 1 →
+ ∃∃I,K,V. |K| = d & L = ⋆.ⓑ{I}V @@ K.
+#d @(nat_ind_plus … d) -d
+[ #L #H
+ elim (length_inv_pos_dx … H) -H #I #K #V #H
+ >(length_inv_zero_dx … H) -H #H destruct
+ @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (**) (* /3/ does not work *)
+| #d #IHd #L #H
+ elim (length_inv_pos_dx … H) -H #I #K #V #H
+ elim (IHd … H) -IHd -H #I0 #K0 #V0 #H1 #H2 #H3 destruct
+ @(ex2_3_intro … (K0.ⓑ{I}V)) //
+]
+qed-.
+
+lemma length_inv_pos_sn_append: ∀d,L. 1 + d = |L| →
+ ∃∃I,K,V. d = |K| & L = ⋆. ⓑ{I}V @@ K.
+#d >commutative_plus @(nat_ind_plus … d) -d
+[ #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct
+ >(length_inv_zero_sn … H1) -K
+ @(ex2_3_intro … (⋆)) // (**) (* explicit constructor *)
+| #d #IHd #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct
+ >H1 in IHd; -H1 #IHd
+ elim (IHd K) -IHd // #J #L #W #H1 #H2 destruct
+ @(ex2_3_intro … (L.ⓑ{I}V)) // (**) (* explicit constructor *)
+ >append_length /2 width=1/
+]
+qed-.
lemma destruct_lpair_lpair: ∀I1,I2,L1,L2,V1,V2. L1.ⓑ{I1}V1 = L2.ⓑ{I2}V2 →
∧∧L1 = L2 & I1 = I2 & V1 = V2.
-#I1 #I2 #L1 #L2 #V1 #V2 #H destruct /2 width=1/
+#I1 #I2 #L1 #L2 #V1 #V2 #H destruct /2 width=1 by and3_intro/
qed-.
lemma discr_lpair_x_xy: ∀I,V,L. L = L.ⓑ{I}V → ⊥.
#I #V #L elim L -L
[ #H destruct
| #L #J #W #IHL #H
- elim (destruct_lpair_lpair … H) -H #H1 #H2 #H3 destruct /2 width=1/ (**) (* destruct lemma needed *)
+ elim (destruct_lpair_lpair … H) -H #H1 #H2 #H3 destruct /2 width=1 by/ (**) (* destruct lemma needed *)
]
qed-.
-
-(* Basic_1: removed theorems 2: chead_ctail c_tail_ind *)
(**************************************************************************)
include "ground_2/notation/functions/append_2.ma".
+include "basic_2/notation/functions/snbind2_3.ma".
+include "basic_2/notation/functions/snabbr_2.ma".
+include "basic_2/notation/functions/snabst_2.ma".
include "basic_2/grammar/lenv_length.ma".
(* LOCAL ENVIRONMENTS *******************************************************)
interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2).
+interpretation "local environment tail binding construction (binary)"
+ 'SnBind2 I T L = (append (LPair LAtom I T) L).
+
+interpretation "tail abbreviation (local environment)"
+ 'SnAbbr T L = (append (LPair LAtom Abbr T) L).
+
+interpretation "tail abstraction (local environment)"
+ 'SnAbst L T = (append (LPair LAtom Abst T) L).
+
definition l_appendable_sn: predicate (lenv→relation term) ≝ λR.
∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2.
#L1 #L2 elim L2 -L2 normalize //
qed.
+lemma ltail_length: ∀I,L,V. |ⓑ{I}V.L| = |L| + 1.
+#I #L #V >append_length //
+qed.
+
+(* Basic_1: was just: chead_ctail *)
+lemma lpair_ltail: ∀L,I,V. ∃∃J,K,W. L.ⓑ{I}V = ⓑ{J}W.K & |L| = |K|.
+#L elim L -L /2 width=5 by ex2_3_intro/
+#L #Z #X #IHL #I #V elim (IHL Z X) -IHL
+#J #K #W #H #_ >H -H >ltail_length
+@(ex2_3_intro … J (K.ⓑ{I}V) W) //
+qed-.
+
(* Basic inversion lemmas ***************************************************)
lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| →
L1 = L2 ∧ K1 = K2.
#K1 elim K1 -K1
-[ * normalize /2 width=1/
+[ * normalize /2 width=1 by conj/
#K2 #I2 #V2 #L1 #L2 #_ <plus_n_Sm #H destruct
| #K1 #I1 #V1 #IH * normalize
[ #L1 #L2 #_ <plus_n_Sm #H destruct
| #K2 #I2 #V2 #L1 #L2 #H1 #H2
elim (destruct_lpair_lpair … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
- elim (IH … H1) -IH -H1 // -H2 /2 width=1/
+ elim (IH … H1) -IH -H1 /2 width=1 by conj/
]
]
qed-.
lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| →
L1 = L2 ∧ K1 = K2.
#K1 elim K1 -K1
-[ * normalize /2 width=1/
+[ * normalize /2 width=1 by conj/
#K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct
normalize in H2; >append_length in H2; #H
elim (plus_xySz_x_false … H)
elim (plus_xySz_x_false … (sym_eq … H))
| #K2 #I2 #V2 #L1 #L2 #H1 #H2
elim (destruct_lpair_lpair … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
- elim (IH … H1) -IH -H1 // -H2 /2 width=1/
+ elim (IH … H1) -IH -H1 /2 width=1 by conj/
]
]
qed-.
lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆.
-#L #K #H
-elim (append_inj_dx … (⋆) … H) //
+#L #K #H elim (append_inj_dx … (⋆) … H) //
qed-.
lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
-#I #L #K #V #H
-elim (append_inj_dx … (⋆.ⓑ{I}V) … H) //
-qed-.
-
-lemma length_inv_pos_dx_append: ∀d,L. |L| = d + 1 →
- ∃∃I,K,V. |K| = d & L = ⋆.ⓑ{I}V @@ K.
-#d @(nat_ind_plus … d) -d
-[ #L #H
- elim (length_inv_pos_dx … H) -H #I #K #V #H
- >(length_inv_zero_dx … H) -H #H destruct
- @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (**) (* /3/ does not work *)
-| #d #IHd #L #H
- elim (length_inv_pos_dx … H) -H #I #K #V #H
- elim (IHd … H) -IHd -H #I0 #K0 #V0 #H1 #H2 #H3 destruct
- @(ex2_3_intro … (K0.ⓑ{I}V)) //
-]
+#I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) //
qed-.
(* Basic_eliminators ********************************************************)
-fact lenv_ind_dx_aux: ∀R:predicate lenv. R (⋆) →
- (∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) →
- ∀d,L. |L| = d → R L.
-#R #Hatom #Hpair #d @(nat_ind_plus … d) -d
-[ #L #H >(length_inv_zero_dx … H) -H //
-| #d #IH #L #H
- elim (length_inv_pos_dx_append … H) -H #I #K #V #H1 #H2 destruct /3 width=1/
-]
-qed-.
-
-lemma lenv_ind_dx: ∀R:predicate lenv. R (⋆) →
- (∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) →
- ∀L. R L.
-/3 width=2 by lenv_ind_dx_aux/ qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma length_inv_pos_sn_append: ∀d,L. 1 + d = |L| →
- ∃∃I,K,V. d = |K| & L = ⋆. ⓑ{I}V @@ K.
-#d >commutative_plus @(nat_ind_plus … d) -d
-[ #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct
- >(length_inv_zero_sn … H1) -K
- @(ex2_3_intro … (⋆)) // (**) (* explicit constructor *)
-| #d #IHd #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct
- >H1 in IHd; -H1 #IHd
- elim (IHd K) -IHd // #J #L #W #H1 #H2 destruct
- @(ex2_3_intro … (L.ⓑ{I}V)) // (**) (* explicit constructor *)
- >append_length /2 width=1/
-]
+(* Basic_1: was: c_tail_ind *)
+lemma lenv_ind_alt: ∀R:predicate lenv.
+ R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) →
+ ∀L. R L.
+#R #IH1 #IH2 #L @(f_ind … length … L) -L #n #IHn * // -IH1
+#L #I #V normalize #H destruct elim (lpair_ltail L I V) /3 width=1 by/
qed-.
⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → ⇩[i] L ≡ K.ⓑ{I}V → ∨∨
(∧∧ yinj i < d & I1 = I & V1 = V) |
(∧∧ (L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ → ⊥) & I1 = I & V1 = V) |
- (∧∧ d ≤ yinj i & L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ & I1 = I & V2 = V)
+ (∧∧ d ≤ yinj i & L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ & I1 = I & V2 = V)
).
interpretation
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/ldrop_append.ma".
+include "basic_2/multiple/llor_ldrop.ma".
+
+(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
+
+lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y.
+/2 width=1 by monotonic_pred/ qed-.
+
+(*
+lemma llor_tail_frees: ∀L1,L2,L,U,d. L1 ⩖[U, d] L2 ≡ L → d < yinj (|L1|) →
+ ∀I1,W1. ⓑ{I1}W1.L1 ⊢ |L1| ϵ 𝐅*[d]⦃U⦄ →
+ ∀I2,W2. ⓑ{I1}W1.L1 ⩖[U, d] ⓑ{I2}W2.L2 ≡ ⓑ{I1}W2.L.
+#L1 #L2 #L #U #d * #HL12 #HL1 #IH #Hd #I1 #W1 #HU #I2 #W2
+@and3_intro [1,2: >ltail_length /2 width=1 by le_S_S/ ]
+#J1 #J2 #J #K1 #K2 #K #V1 #V2 #V #i #HLK1 #HLK2 #HLK
+lapply (ldrop_fwd_length_lt2 … HLK1) >ltail_length #H
+lapply (lt_plus_SO_to_le … H) -H #H
+elim (le_to_or_lt_eq … H) -H #H
+[ elim (ldrop_O1_lt (Ⓕ) … H) #Z1 #Y1 #X1 #HLY1
+ elim (ldrop_O1_lt (Ⓕ) L2 i) [2: /2 width=3 by lt_to_le_to_lt/ ] #Z2 #Y2 #X2 #HLY2
+ elim (ldrop_O1_lt (Ⓕ) L i) // #Z #Y #X #HLY
+ lapply (ldrop_O1_inv_append1_le … HLK1 … HLY1) /2 width=1 by lt_to_le/ -HLK1 normalize #H destruct
+ lapply (ldrop_O1_inv_append1_le … HLK2 … HLY2) /3 width=3 by lt_to_le_to_lt, lt_to_le/ -HLK2 normalize #H destruct
+ lapply (ldrop_O1_inv_append1_le … HLK … HLY) /2 width=1 by lt_to_le/ -HLK normalize #H destruct
+ elim (IH … HLY1 HLY2 HLY) -IH -HLY1 -HLY2 -HLY *
+ [ /3 width=1 by and3_intro, or3_intro0/
+ | #HnU #HZ #HX
+ | #Hdi #H2U #HZ #HX
+ ]
+| -IH destruct
+ lapply (ldrop_O1_inv_append1_le … HLK1 … (⋆) ?) // -HLK1 normalize #H destruct
+ lapply (ldrop_O1_inv_append1_le … HLK2 … HL12)
+ lapply (ldrop_O1_inv_append1_le … HLK … (⋆) ?) // -HLK normalize #H destruct
+ @or3_intro2 @and4_intro /2 width=1 by ylt_fwd_le/
+]
+*)
(* Advanced properties ******************************************************)
+lemma llor_skip: ∀L1,L2,U,d. |L1| ≤ |L2| → yinj (|L1|) ≤ d → L1 ⩖[U, d] L2 ≡ L1.
+#L1 #L2 #U #d #HL12 #Hd @and3_intro // -HL12
+#I1 #I2 #I #K1 #K2 #K #W1 #W2 #W #i #HLK1 #_ #HLK -I2 -L2 -K2
+lapply (ldrop_mono … HLK … HLK1) -HLK #H destruct
+lapply (ldrop_fwd_length_lt2 … HLK1) -K1
+/5 width=3 by ylt_yle_trans, ylt_inj, or3_intro0, and3_intro/
+qed.
+
axiom llor_total: ∀L1,L2,T,d. |L1| ≤ |L2| → ∃L. L1 ⩖[T, d] L2 ≡ L.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⓓ term 55 T . break term 55 L )"
+ non associative with precedence 55
+ for @{ 'SnAbbr $T $L }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⓛ term 55 T . break term 55 L )"
+ non associative with precedence 55
+ for @{ 'SnAbst $T $L }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⓑ { term 46 I } break term 55 T . break term 55 L )"
+ non associative with precedence 55
+ for @{ 'SnBind2 $I $T $L }.
normalize /4 width=1 by ldrop_drop, monotonic_pred/
qed.
+lemma ldrop_O1_eq: ∀L,s. ⇩[s, 0, |L|] L ≡ ⋆.
+#L elim L -L /2 width=1 by ldrop_drop, ldrop_atom/
+qed.
+
lemma ldrop_split: ∀L1,L2,d,e2,s. ⇩[s, d, e2] L1 ≡ L2 → ∀e1. e1 ≤ e2 →
∃∃L. ⇩[s, d, e2 - e1] L1 ≡ L & ⇩[s, d, e1] L ≡ L2.
#L1 #L2 #d #e2 #s #H elim H -L1 -L2 -d -e2
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/grammar/lenv_append.ma".
+include "basic_2/substitution/ldrop.ma".
+
+(* DROPPING *****************************************************************)
+
+(* Properties on append for local environments ******************************)
+
+fact ldrop_O1_append_sn_le_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 →
+ d = 0 → e ≤ |L1| →
+ ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2.
+#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e normalize
+[2,3,4: /4 width=1 by ldrop_skip_lt, ldrop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ]
+#d #e #_ #_ #H <(le_n_O_to_eq … H) -H //
+qed-.
+
+lemma ldrop_O1_append_sn_le: ∀L1,L2,s,e. ⇩[s, 0, e] L1 ≡ L2 → e ≤ |L1| →
+ ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2.
+/2 width=3 by ldrop_O1_append_sn_le_aux/ qed.
+
+(* Inversion lemmas on append for local environments ************************)
+
+lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K →
+ |L2| ≤ e → ⇩[s, 0, e - |L2|] L1 ≡ K.
+#K #L1 #L2 elim L2 -L2 normalize //
+#L2 #I #V #IHL2 #s #e #H #H1e
+elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HL12 destruct
+[ lapply (le_n_O_to_eq … H1e) -H1e -IHL2
+ >commutative_plus normalize #H destruct
+| <minus_plus >minus_minus_comm /3 width=1 by monotonic_pred/
+]
+qed-.
+
+lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → e ≤ |L2| →
+ ∀K2. ⇩[s, 0, e] L2 ≡ K2 → K = L1 @@ K2.
+#K #L1 #L2 elim L2 -L2 normalize
+[ #s #e #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2
+ #H2 elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct
+ >(ldrop_inv_O2 … H1) -H1 //
+| #L2 #I #V #IHL2 #s #e @(nat_ind_plus … e) -e [ -IHL2 ]
+ [ #H1 #_ #K2 #H2
+ lapply (ldrop_inv_O2 … H1) -H1 #H1
+ lapply (ldrop_inv_O2 … H2) -H2 #H2 destruct //
+ | /4 width=7 by ldrop_inv_drop1, le_plus_to_le_r/
+ ]
+]
+qed-.
}
]
[ { "basic local env. slicing" * } {
- [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_leq" + "ldrop_ldrop" * ]
+ [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_append" + "ldrop_leq" + "ldrop_ldrop" * ]
}
]
[ { "basic term relocation" * } {
projects / helm.git / commitdiff