proposition: Theorem ptree_ind' : forall P : ptree -> Prop, (forall v l, Forall P l -> P (PTsome v l)) -> forall t, P t.
proof: Proof. intros P H. fix IH 1. intros [v l]. apply H. induction l ; constructor. apply IH. apply IHl. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)