fact: Fixpoint stable (l1 l2:ab_env) {struct l1} : bool := match l1, l2 with nil, nil => true | (s,v)::tl1, (_,v')::tl2 => Ab.eq v v' && stable tl1 tl2 | _, _ => false end.
imports: syntax little denot Bool List String ZArith axiom