proposition: Lemma f_equal_snd_injective_projections' {A B x y} (p : fst x = fst y :> A) (q : snd x = snd y :> B) : f_equal snd (injective_projections' p q) = q.
proof: Proof. destruct x, y; simpl in *; destruct p, q; reflexivity. Defined.
imports: Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Coq.Arith.PeanoNat Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Common