- elim t; simplify in f f1;
- [ 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))
+ elim a; simplify in f f1;
+ [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
+ |2,4: cases x;
+ [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))