proposition: Lemma tree_value_extent T E E': treep T -> (forall i, i<=c (tree_size T) -> Vg E i = Vg E' i) -> tree_value E T = tree_value E' T.
proof: Proof. set P := (tree_value_prop E) ; set P' := (tree_value_prop E'). move: T; apply:tree_ind. - move => n nN h. rewrite(proj31 P n nN) (proj31 P' n nN); apply: h. rewrite (proj31 tree_size_p _ nN); exact: (cleR (CS_nat nN)). - move => x tp h1; rewrite (proj32 tree_size_p x tp) => h2. by rewrite(proj32 P x tp) (proj32 P' x tp); rewrite (h1 h2). - move => x x' tp tp'. rewrite (proj33 tree_size_p x x' tp tp') => h1 h2 h3. rewrite (proj33 P x x' tp tp') (proj33 P' x x' tp tp'). move:(Nmax_p1 (NS_tree_size tp) (NS_tree_size tp'))=> [ma mb mc]. have q1: forall i, i <=c tree_size x -> Vg E i = Vg E' i. move => i li1; exact: (h3 _ (cleT li1 mb)). have q1': forall i, i <=c tree_size x' -> Vg E i = Vg E' i. move => i li1; exact: (h3 _ (cleT li1 mc)). by rewrite h1 // h2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)