aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/1322.v
blob: 1ec7d452a653785f4f126e5e1423225af906fcc6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
Require Import Setoid.

Section transition_gen.

Variable I : Type.
Variable I_eq :I -> I -> Prop.
Variable I_eq_equiv : Setoid_Theory I I_eq.

(* Add Relation I I_eq
  reflexivity proved by I_eq_equiv.(Seq_refl I I_eq)
  symmetry proved by I_eq_equiv.(Seq_sym I I_eq)
  transitivity proved by I_eq_equiv.(Seq_trans I I_eq)
as I_eq_relation. *)

Add Setoid I I_eq I_eq_equiv as I_with_eq.

Variable F : I -> Type.
Variable F_morphism : forall i j, I_eq i j -> F i = F j.


Add Morphism F with signature I_eq ==> (@eq _) as F_morphism2.
Admitted.

End transition_gen.