#k #p #B #nil #op #f #g (elim k) [normalize @nill]
-k #k #Hind (cases (true_or_false (p k))) #H
[>bigop_Strue // >bigop_Strue // >bigop_Strue //
#k #p #B #nil #op #f #g (elim k) [normalize @nill]
-k #k #Hind (cases (true_or_false (p k))) #H
[>bigop_Strue // >bigop_Strue // >bigop_Strue //