one more

mit-plv · Jul 26, 2023 · 059a190 · 059a190
1 parent 6c397e1
commit 059a190
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/bedrock2/src/bedrock2/bottom_up_simpl.v b/bedrock2/src/bedrock2/bottom_up_simpl.v
@@ -461,7 +461,7 @@ Module List.
 
     Lemma apps_concat: forall (xss: list (list A)), apps xss = List.concat xss.
     Proof.
-      induction xss. 1: reflexivity.
+      induction xss > [ reflexivity | ].
       simpl. rewrite <- IHxss.
       destruct xss; try reflexivity.
       simpl. symmetry. apply List.app_nil_r.
@@ -509,7 +509,7 @@ Module List.
       intros. subst. rewrite 2apps_concat. revert i xss H.
       induction n; intros; simpl in *.
       - rewrite 2List.upto_beginning; trivial.
-      - destruct xss. 1: reflexivity.
+      - destruct xss > [ reflexivity | ].
         simpl in *.
         rewrite 2upto_app. f_equal. apply IHn. lia.
     Qed.