diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-03 15:37:11 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-03 15:37:11 -0500 |
| commit | c58be98d96ee31cff34cc30b7f5958f231fc456e (patch) | |
| tree | f23dff8c6d92617efc519389dd14ab3e12c460a8 /src/Reflection/Relations.v | |
| parent | 71a39be019badfdc3b5e66f39a13338d20980eab (diff) | |
Add interp_flat_type_rel_pointwise2_hetero_iff
Diffstat (limited to 'src/Reflection/Relations.v')
| -rw-r--r-- | src/Reflection/Relations.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Reflection/Relations.v b/src/Reflection/Relations.v index 3b7b8e104..9808145b7 100644 --- a/src/Reflection/Relations.v +++ b/src/Reflection/Relations.v @@ -166,6 +166,11 @@ Section language. := @interp_flat_type_rel_pointwise2_gen_Prop Prop and True. Global Arguments interp_flat_type_rel_pointwise2 _ !_ _ _ / . + Lemma interp_flat_type_rel_pointwise2_hetero_iff {R t} x y + : interp_flat_type_rel_pointwise2 (fun t => R t t) t x y + <-> interp_flat_type_rel_pointwise2_hetero R t t x y. + Proof. induction t; simpl; rewrite_hyp ?*; reflexivity. Qed. + Section with_coercion. Let Tbase := (@Tbase base_type_code). Local Coercion Tbase : base_type_code >-> flat_type. |