X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FGeneral.v;h=7aefcf020ee6114dc3b2af3d22e5a0cd281c6a08;hb=5a92232f20931ebb060082d5236239c2d2061e17;hp=ffd0d29662a00a2bd143b2e5307b1f1bf40e3b39;hpb=90316bd3f95d22815f987ccc8db23b7b04f45efe;p=coq-hetmet.git

diff --git a/src/General.v b/src/General.v
index ffd0d29..7aefcf0 100644
--- a/src/General.v
+++ b/src/General.v
@@ -301,6 +301,16 @@ Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A :=
     | (a::b) => (unleaves'' b),,(T_Leaf a)
   end.
 
+Lemma mapleaves {T:Type}(t:Tree ??T){Q}{f:T->Q} : leaves (mapOptionTree f t) = map f (leaves t).
+  induction t.
+  destruct a; auto.
+  simpl.
+  rewrite IHt1.
+  rewrite IHt2.
+  rewrite map_app.
+  auto.
+  Qed.
+
 Fixpoint filter {T:Type}(l:list ??T) : list T :=
   match l with
     | nil => nil