blob: 01c06f2c40819d602c7e94af91efc17e964048c5 (
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.
|
