lambdapi
lambdapi copied to clipboard
Induction command does not work on vectors
require open Stdlib.Set Stdlib.Prop Stdlib.Nat Stdlib.List;
symbol A:TYPE;
inductive V:ℕ → TYPE ≔ Vnil:V 0 | Vcons (x:A) n (v:V n):V(n +1);
symbol sample_2 n (v : V n) : π ⊤ ≔
begin
induction and assume n; induction fail