Box and cap tactics

[favonia]

Close #410, mostly.

[favonia]

BTW, this works in this PR:

def lemma0
  (A : [i] type [])
  (B : [i] type [i=0 → A 0])
  (C : [i] type [i=0 → A 1])
  : type
  = [i] (comp 0 1 (A i) [i=0 → B | i=1 → C]) []

def lemma1
  (A : [i] type [])
  (B : [i] type [i=0 → A 0])
  (C : [i] type [i=0 → A 1])
  (b : B 1)
  (c : C 1)
  (a : [i] A i [i = 0 → coe 1 0 b in B | i = 1 → coe 1 0 c in C])
  : lemma0 A B C
  = λ i → box (a i) [b | c]

def lemma2
  (A : [i] type [])
  (B : [i] type [i=0 → A 0])
  (C : [i] type [i=0 → A 1])
  (b : B 1)
  (c : C 1)
  (a : [i] A i [i = 0 → coe 1 0 b in B | i = 1 → coe 1 0 c in C])
  : [i] A i []
  = λ i → lemma1 A B C b c a i .cap

[favonia]

@ecavallo please feel free to hijack this PR and put in some reasonable names.