%%% Connective

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

%%% Inference Rules

tensorl : (hyp (A tensor B) -o conc C) 
	   o- (hyp A -o hyp B -o conc C).

tensorr : conc (A tensor B) 
	   o- conc A
	   o- conc B.

%%% Principal Cases

ca/tensor1 : ca (B1 tensor B2) (tensorr ^ D2 ^ D1) 
	      ([h:^ (hyp (B1 tensor B2))] tensorl ^ E ^ h) F
	      <- ({a2 : w}{h2 : hyp B2 @ a2} ca B1 D1 
		    ([a1 : w][h1 : hyp B1 @ a1] E a1 h1 a2 h2) (E' a2 h2))
	      <- ca B2 D2 ([a2 : w][h2 : hyp B2 @ a2] E' a2 h2) F.


%%% D-Commutative Cases

cad/tensorl  : ca A (tensorl ^ D ^ H) E (tensorl ^ D' ^ H)
		<- ({a1 : w} {h1 : hyp _ @ a1}
		    {a2 : w} {h2 : hyp _ @ a2}
		      ca A (D a1 h1 a2 h2) E (D' a1 h1 a2 h2)).

%%% E-Commutative Cases

cae/tensorl  : ca A D 
		([a : w] [h : hyp _ @ a] tensorl ^ (E a h) ^ H) 
		(tensorl ^ E' ^ H)
		<- ({a1 : w} {h1 : hyp _ @ a1}
		    {a2 : w} {h2 : hyp _ @ a2}
		      ca A D
		      ([a : w] [h : hyp _ @ a] E a h a1 h1 a2 h2) 
		      (E' a1 h1 a2 h2)).

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

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