proposition: Lemma quote_neg_ok@{} (V:Type0) (v : Vars V) n (V':Type0) (v' : Vars V') `{!Quote v n v'} : eval (merge v v') (Neg (quote n)) = almost_negate n.
proof: Proof. simpl. apply ap,eval_quote. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra