2014-10-01 21:02:49 +00:00
|
|
|
import logic
|
|
|
|
|
|
|
|
|
|
inductive tree (A : Type) :=
|
2015-02-26 01:00:10 +00:00
|
|
|
leaf : A → tree A|
|
2014-10-01 21:02:49 +00:00
|
|
|
node : tree A → tree A → tree A
|
|
|
|
|
|
|
|
|
|
namespace tree
|
|
|
|
|
|
|
|
|
|
definition below_rec {A : Type} (t : tree A) {P : tree A → Type} (iH : Π (t : tree A), P t) : P t :=
|
|
|
|
|
have general : ∀ (t : tree A),
|
|
|
|
|
P t, from
|
|
|
|
|
-- take t, iH t,
|
|
|
|
|
sorry,
|
|
|
|
|
general t
|
|
|
|
|
|
|
|
|
|
end tree
|
