-[ #k1 #H1 #H2 destruct -Y0;
- lapply (tpr_inv_sort1 … H1) -H1
-(* case 1: sort, sort *)
- #H1 destruct -X2 //
-| #i1 #H1 #H2 destruct -Y0;
- lapply (tpr_inv_lref1 … H1) -H1
-(* case 2: lref, lref *)
+[ #I1 #H1 #H2 destruct -Y0;
+ lapply (tpr_inv_atom1 … H1) -H1
+(* case 1: atom, atom *)