fact: Fixpoint join_env (l1 l2:ab_env) {struct l1} : ab_env := match l1,l2 with nil,nil => nil | (s,i)::tl1, (_,i')::tl2 => (s,Ab.join i i')::join_env tl1 tl2 | _, _ => nil end.
imports: syntax little denot Bool List String ZArith axiom