(<*a,(b ")*> ") . 2 = (<*a,(b ")*> . 2) " by VALUED_1:10;
hence (<*a,(b ")*> ") . 2 = b ; :: thesis: verum