- #v #p1 elim p1 normalize
- [ #p2 elim p2 normalize
- [ #x cases x normalize //
- | #dir #path #IH #x elim x normalize
- [ #n cases dir normalize
-
-
- #p2 elim p normalize
- [ #t elim t normalize //
- | * normalize
- [ #path #IH
-
-
- #path #IH #x elim x normalize
- [ #v cases res normalize lapply (IH (leaf v)) -IH elim path
- normalize // * normalize
- [2: #path' #IH #IH2 @IH
\ No newline at end of file
+ #v #p1 #p2 #t @pair_elim #t' #res #EQ inversion (admissible t (reverse … p1 @ p2))
+ [ #H >update_correct2 // whd in ⊢ (??%?);
+ >(reverse_append ? (reverse ? p2) p1) >reverse_reverse >EQ %
+ | #H >update_correct1 // >setleaf_fun_correct in EQ; // ]
+qed.
\ No newline at end of file