+ #Hqin % [ @Hqin ] -Hqin
+ lapply (append_l2_injective … HT) [ >Hlenqin @Hlenqin0 ] -HT #HT
+ lapply (cons_injective_l ????? HT) #Hcin % [ @Hcin ] -Hcin
+ lapply (cons_injective_r ????? HT) -HT #HT
+ lapply (cons_injective_r ????? HT) -HT
+ >associative_append >associative_append #HT
+ lapply (append_l1_injective … HT) [ >Hlenqout @Hlenqout0 ]
+ #Hqout % [ @Hqout ] -Hqout
+ lapply (append_l2_injective … HT) [ >Hlenqout @Hlenqout0 ] -HT normalize #HT
+ lapply (cons_injective_l ????? HT) #Hcout % [ @Hcout ] -Hcout
+ lapply (cons_injective_r ????? HT) -HT #HT
+ lapply (cons_injective_r ????? HT) -HT #HT
+ lapply (cons_injective_l ????? HT) #Hmv % [ @Hmv ] -Hmv
+ @(cons_injective_r ????? HT) ]
+ -HT * #Hqin * #Hcin * #Hqout * #Hcout * #Hmv #HT0
+ >(?:qin0@(〈cin0,false〉::〈comma,false〉::qout0@[〈cout0,false〉;〈comma,false〉;〈mv0,false〉])@〈bar,false〉::T0
+ = mk_tuple qin cin qout cout mv@〈bar,false〉::T0)
+ [|>Hqin >Hqout >Hcin >Hcout >Hmv normalize >associative_append >associative_append
+ normalize >associative_append % ]
+ %
+ | #c0 #cs0 #HT cut (∃cs1.c0::cs0 = tuple@〈bar,false〉::cs1)
+ [ cases (append_eq_tech1 ?????? HT ?)
+ [ -HT #ta #Hta cases (append_eq_tech2 … Hta ?)
+ [ -Hta #tb #Htb %{tb} @Htb
+ | @daemon ]
+ | @le_S_S >length_append >(plus_n_O (|tuple|)) >commutative_plus @le_plus
+ [ @le_O_n
+ | >Htuple normalize >length_append >length_append @le_plus [ >Hlenqin >Hlenqin0 % ]
+ @le_S_S @le_S_S >length_append >length_append @le_plus [ >Hlenqout >Hlenqout0 % ] %] ]
+ ]
+ * #cs1 #Hcs1 >Hcs1 in HT; >associative_append >associative_append #HT
+ lapply (append_l2_injective … HT) // -HT #HT
+ lapply (cons_injective_r ????? HT) -HT
+ <associative_append #HT >Htuple %2 @(IH ?? HT)
+ ]
+]
+qed.
+
+lemma no_grids_in_tuple : ∀n,l.tuple_TM n l → no_grids l.
+#n #l * #qin * #cin * #qout * #cout * #mv * * * * * * * * * *
+#_ #_ #Hqin #Hqout #Hcin #Hcout #Hmv #_ #_ #_ #Hl >Hl
+#c #Hc normalize in Hc; cases (memb_append … Hc) -Hc #Hc
+[ @bit_not_grid @(Hqin … Hc)
+| cases (orb_true_l … Hc) -Hc #Hc
+[ change with (c == 〈cin,false〉 = true) in Hc; >(\P Hc) @bit_or_null_not_grid //
+| cases (orb_true_l … Hc) -Hc #Hc
+[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) %
+| cases (memb_append …Hc) -Hc #Hc
+[ @bit_not_grid @(Hqout … Hc)
+| cases (orb_true_l … Hc) -Hc #Hc
+[ change with (c == 〈cout,false〉 = true) in Hc; >(\P Hc) @bit_or_null_not_grid //
+| cases (orb_true_l … Hc) -Hc #Hc
+[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) %
+| >(memb_single … Hc) @bit_or_null_not_grid @Hmv
+]]]]]]
+qed.
+
+lemma no_marks_in_tuple : ∀n,l.tuple_TM n l → no_marks l.
+#n #l * #qin * #cin * #qout * #cout * #mv * * * * * * * * * *
+#Hqin #Hqout #_ #_ #_ #_ #_ #_ #_ #_ #Hl >Hl
+#c #Hc normalize in Hc; cases (memb_append … Hc) -Hc #Hc
+[ @(Hqin … Hc)
+| cases (orb_true_l … Hc) -Hc #Hc
+[ change with (c == 〈cin,false〉 = true) in Hc; >(\P Hc) %
+| cases (orb_true_l … Hc) -Hc #Hc
+[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) %
+| cases (memb_append … Hc) -Hc #Hc
+[ @(Hqout … Hc)
+| cases (orb_true_l … Hc) -Hc #Hc
+[ change with (c == 〈cout,false〉 = true) in Hc; >(\P Hc) %
+| cases (orb_true_l … Hc) -Hc #Hc
+[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) %
+| >(memb_single … Hc) %
+]]]]]]
+qed.