| whd; simplify; intros; cases x; apply I;
| whd; simplify; intros 2; cases x; cases y; simplify; intros; assumption;
| whd; simplify; intros 3; cases x; cases y; cases z; simplify; intros;
| whd; simplify; intros; cases x; apply I;
| whd; simplify; intros 2; cases x; cases y; simplify; intros; assumption;
| whd; simplify; intros 3; cases x; cases y; cases z; simplify; intros;