%%% Connective

and    : o -> o -> o.  %infix right 11 and.

%%% Inference Rules

andl1 : (hyp (A and B) -o conc C)
        o- (hyp A -o conc C).
andl2 : (hyp (A and B) -o conc C)
        o- (hyp B -o conc C).

andr : {a : w} 
	conc (A and B) @ a
	<- conc B @ a
	<- conc A @ a.

%%% Principal Cases

ca/and1 : ca (A1 and A2) (andr ^ D1 D2) 
	   ([h:^ (hyp (A1 and A2))] andl1 ^ E ^ h) F
	   <- ca A1 D1 E F.


ca/and2 : ca (A1 and A2) (andr ^ D1 D2) 
	   ([h :^ (hyp (A1 and A2))] andl2 ^ E ^ h) F
	   <- ca A2 D2 E F.


%%% D-Commutative Cases

cad/andl1  : ca A (andl1 ^ D1 ^ H) E (andl1 ^ D1' ^ H)
	      <- {a : w} {h1: hyp B1 @ a} ca A (D1 ^ h1) E (D1' ^ h1).


cad/andl2  : ca A (andl2 ^ D2 ^ H) E (andl2 ^ D2' ^ H)
	      <- {a : w} {h2:hyp B2 @ a} ca A (D2 ^ h2) E (D2' ^ h2).

%%% E-Commutative Cases

cae/andr : ca A D ([h:^ (hyp A)] andr ^ (E1 ^ h) (E2 ^ h)) (andr ^ E1' E2')
	    <- ca A D E1 E1'
	    <- ca A D E2 E2'.

cae/andl1 : ca A D
         ([a0:w] [h:hyp A @ a0]
             andl1 ^ ([a1:w] [h1:hyp A3 @ a1] E1 ^ h ^ h1) HP H) (andl1 ^ E1' ^ H)
	     <- ({a1:w}{h1 : hyp A3 @ a1} ca A D ([a0:w] [h:hyp A @ a0] E1 a0 h a1 h1) (E1' ^ h1)).

cae/andl2 : ca A D
         ([a0:w] [h:hyp A @ a0]
             andl2 ^ ([a1:w] [h1:hyp A3 @ a1] E2 ^ h ^ h1) HP H) (andl2 ^ E2' ^ H)
	     <- ({a1:w}{h1 : hyp A3 @ a1} ca A D ([a0:w] [h:hyp A @ a0] E2 a0 h a1 h1) (E2' ^ h1)).