enrich
   tree, 
   list
with
   predicates 
       . ∈ . : List[Bool] × Tree[A];
   
   variables 
       b : Bool;
       t : Tree[A];
       p : List[Bool];
       a : A;
   
   partial functions 
       . ( . ) : Tree[A] × List[Bool] → Tree[A] with λ t, p. p ∈ t;
       . ( . := . ) : Tree[A] × List[Bool] × Tree[A] → Tree[A] with λ t, p, t0. p ∈ t;
   
   
   axioms 
      get-base: t([]) = t;
      used for: s, ls;
      
      get-rec: branch(t1, a, t2)(b ' + p) = (b ⊃ t2(p);t1(p));
      used for: s, ls;
      
      put-base: t([] := t0) = t0;
      used for: s, ls;
      
      put-rec: branch(t1, a, t2)(b ' + p := t0) = (b ⊃ branch(t1, a, t2(p := t0));branch(t1(p := t0), a, t2));
      used for: s, ls;
      
      in-base: p ∈ leaf ↔ p = [];
      used for: s, ls;
      
      empty-rec: [] ∈ t;
      used for: s, ls;
      
      in-rec: b ' + p ∈ branch(t1, a, t2) ↔ p ∈ (b ⊃ t2;t1);
      used for: s, ls;
   
   
end enrich