X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=ee5cb1690a13480f641daa7d808a7f20fd2925db;hp=ae27b9f99cc725f7b68a5a2cf719e83421825146;hb=91f06dc68cf5888360f1819429b10e054f94b243;hpb=a3592b805c570883fd63a5c75d6e16ea83f2e849

diff --git a/src/General.v b/src/General.v
index ae27b9f..ee5cb16 100644
--- a/src/General.v
+++ b/src/General.v
@@ -106,6 +106,11 @@ Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tre
   end.
 Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
   forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.
+Lemma mapOptionTree_distributes
+  : forall T R (a b:Tree ??T) (f:T->R),
+    mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
+  reflexivity.
+  Qed.
 
 Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
   match tt with
@@ -520,6 +525,12 @@ Fixpoint takeT {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) :=
       end
   end.
 
+Definition takeT' {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
+  match takeT tf with
+    | None   => []
+    | Some x => x
+  end.
+
 (* lift a function T->bool to a function (option T)->bool by yielding (None |-> b) *)
 Definition liftBoolFunc {T}(b:bool)(f:T -> bool) : ??T -> bool :=
   fun t =>