proposition: Lemma Tree_value_compat E e: tree_value E (Tree_to_tree e) = Tree_value E e.
proof: Proof. move:(tree_value_prop E) => [ha hb hc]. have H0 x: treep (Tree_to_tree x) by case: (Tree_to_tree_prop x). elim:e. - by move => n /=; rewrite ha //; apply: nat_to_B_Nat. - by move => t h /=; rewrite -h hb //. - by move => t h t' h' /=; rewrite - h - h' hc //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)