|#G1 #A #i #t1 #_ #P @(ex_intro … i) @(weak … t1 t1)
|#G1 #A #B #C #i #t1 #t2 #H1 #H2 #H3 (cases (H1 ?) )
[#i #Bi @(ex_intro … i) @(weak … Bi t2)
|#G1 #A #i #t1 #_ #P @(ex_intro … i) @(weak … t1 t1)
|#G1 #A #B #C #i #t1 #t2 #H1 #H2 #H3 (cases (H1 ?) )
[#i #Bi @(ex_intro … i) @(weak … Bi t2)