proposition: Lemma Ain_mor s s' t t' : Aeq s s' -> Aeq t t' -> Ain s t -> Ain s' t'.
proof: Proof. intros H1 H2 H3. destruct t as [B1 g1]. simpl in H3. destruct H3 as [b1 H3]. destruct t' as [B2 g2]. simpl. simpl in H2. destruct H2 as [H2 _]. destruct (H2 b1) as [b2 H4]. exists b2. rewrite <- H4. now rewrite <- H1. Qed.
imports: Setoid Morphisms