- [#i #j #Aij #P #H destruct
- |#G1 #A #i #t1 #_ #P #H destruct
- |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #P #H3
- cases (lift_D … H3) #P * #eqP #eqA >eqP @(weak … i) /2/
- |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #P #H destruct
- |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #H destruct
- |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #H destruct
- |#G1 #A #B #C #i #ch #t1 #t2 #H #_ #P #H
+ [#i #j #Aij #P #Q #H destruct
+ |#G1 #A #i #t1 #_ #P #Q #H destruct
+ |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #P #Q #H3
+ cases (lift_D … H3) #P1 * #Q1 * * #eqP #eqQ #eqA
+ >eqP @(weak … i) /2/
+ |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #P #Q #H destruct
+ |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #Q #H destruct
+ |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #Q #H destruct
+ |#G1 #A #B #C #i #ch #t1 #t2 #H #_ #P #Q #H