- [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
- | elim t1;
- [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
- | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
- ]
- | exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
- | elim t1;
- [ exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
- | exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
+ [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
+ |2,4: cases t1;
+ [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
+ |2,4: exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))