% Canonical forms

%theorem ss_cn : forall* {A:o} {S: solve A} {D: pf A}
	         forall {SS : s_sound S D}
	         exists {CN : can A D} true.
%theorem hs_at : forall* {A:o} {H : assume A}{D : pf A}
	         forall {HS : h_sound H D}
	         exists {ATH :  atm D} true.
%theorem is_at : forall* {A : o} {P : p}{I : A >> P} {D : (pf A -> pf (atom P))} 
	         forall {IS : i_sound I D}
	         exists {ATI : ({u:pf A} atm u -> atm (D u))} true.
%prove 4 (SS HS IS) 
  (ss_cn SS _) 
  (hs_at HS _) 
  (is_at IS _).

%terminates (SS HS IS) (ss_cn SS _) 
		       (hs_at HS _) 
		       (is_at IS _).