proposition: Lemma isReflSwapping_cons : forall {G} {vc : VarSym G} a b (s : Swapping vc), isReflSwapping ((a,b)::s) <=> a = b # isReflSwapping s.
proof: Proof. unfold isReflSwapping; introv; simpl; split; intro k; cpx. repnd; allrw; sp. Qed.
imports: Swap AssociationList Eqdep_dec