33 lines
1.1 KiB
Text
33 lines
1.1 KiB
Text
open tactic
|
||
|
||
example (a b : nat) (s t : list nat) : a::s = b::t → a ≠ b → false :=
|
||
by cc
|
||
|
||
example (a b : nat) (s t : list nat) : a::s = b::t → t ≠ s → false :=
|
||
by cc
|
||
|
||
example (a c b : nat) (s t : list nat) : a::s = b::t → a ≠ c → c = b → false :=
|
||
by cc
|
||
|
||
example (a c b : nat) (s t : list nat) : a::a::s = a::b::t → a ≠ c → c = b → false :=
|
||
by cc
|
||
|
||
example (a b : nat) (s t r : list nat) : a::s = r → r = b::t → a ≠ b → false :=
|
||
by cc
|
||
|
||
example (a b : nat) (s t r : list nat) : a::s = r → r = b::t → a = b :=
|
||
by cc
|
||
|
||
universe variables u
|
||
inductive Vec (α : Type u) : nat → Type (max 1 u)
|
||
| nil : Vec 0
|
||
| cons : ∀ {n}, α → Vec n → Vec (nat.succ n)
|
||
|
||
example (α : Type u) (a b c d : α) (n : nat) (s t : Vec α n) : Vec.cons a s = Vec.cons b t → a ≠ b → false :=
|
||
by cc
|
||
|
||
example (α : Type u) (a b c d : α) (n : nat) (s t : Vec α n) : Vec.cons a s = Vec.cons b t → t ≠ s → false :=
|
||
by cc
|
||
|
||
example (α : Type u) (a b c d : α) (n : nat) (s t : Vec α n) : Vec.cons a (Vec.cons a s) = Vec.cons a (Vec.cons b t) → b ≠ c → c = a → false :=
|
||
by cc
|