Goal:
  
  A : Type
  P : nat → A → Type
  n : nat
  n0 : nat
  hd : A
  tl : list A
  p : P (n + n0) hd
  X : Alli (λ x : nat, P (n + x)) (S n0) tl
  IHX : Alli P (S (n + n0)) tl
  ============================
   (Alli P (S (n + n0)) tl)


DEBUG:Going to execute:
solve
[ trivial
with eq_true
| reflexivity
| symmetry; trivial
| contradiction
| congruence ]