S and F continuations are conjunction of goals: C contains the splittable goal with the currant covering of type, say cont. split
guesses a *simultaneous* (not sequential) splitting for all the extensional varianles in the context of the current splitting continuation. Update deepens the covering.
This is *eager* splitting: we split immediately after CASE,
even if other rules are available and record the backtracking point with the current covering. On clash-failure, the top of the continuation is copied and the covering is updated. There is no finite failure: deeper and deeper coverings are produced.


i,o,cont:type.
o<cont.

demo 	: o  -> type.
prove 	: o -> o -> o -> cont-> type.
assume 	: o -> type.
chain  	: o -> o -> o -> o -> cont-> type.
split		: o -> cont-> o-> type.
update	: cont -> cont -> type.

start 	: demo A <- prove A true false false.
ptrue   	: prove true true _ _.				%one answer
%pnot	 : prove (not A) S F C <- prove (A => false) S F C.
pand     	 : prove (A & B) S F C <- prove A (B & S) F C.
porl		 : prove (A v B ) S F C <- prove A S (B v F) C.
pimplies 	 : prove (A => B) S F C <- (assume A -> prove B S F C).
pinst	 : prove (some A) S F C <- prove (A X) S F C.
pgen		 : prove (pi A) S F C <- {a : i} prove (A a) S F C.
pcase	 : prove (all A) S F C 
			<-  split (all A)  C Gs 
			<- prove Gs S F (all A & C).
patom    	 : prove A S F C <- assume B <- chain B A S F C.
pbtrack  	:  prove A S (F & false) C <- prove F S false C.
psplit  	:  prove A S false C
			<- update C NC
			<- prove C S false NC.

uaxiom 	 : chain A A S F C<- prove S true F C.
uandL   	 : chain (B1 & B2) A S F C <- chain B1 A S F C.
uandR   	 : chain (B1 & B2) A S F C <- chain B2 A S F C.
uall     	 : chain (all D) A S F C <- chain (D X) A S F C.
uimplies 	 : chain (B => A) A  S F C <- prove B S F C.

ts		: split (all A) C (Gs &Gss)	
			<- {a:i} cover (A a) C Gs
			<- split0 (A a) C Gss.
s0_step	: split0 (A &B) C (Gs & Gss)
			<- split A C Gs
			<- split0 B C Gss
s0_base		: split0 A C Gs 
			<- split A C Gs.