Skip to content

Commit 3acee34

Browse files
authored
Merge pull request #54 from Mbodin/master
Adding a way to convert [member]s into [In]s.
2 parents adc7c70 + 915a186 commit 3acee34

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

theories/Data/Member.v

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -132,4 +132,9 @@ Section member.
132132
eapply IHm in H. rewrite H. reflexivity. } }
133133
Qed.
134134

135+
Lemma member_In : forall ls (t : T), member t ls -> List.In t ls.
136+
Proof.
137+
induction 1; simpl; auto.
138+
Qed.
139+
135140
End member.

0 commit comments

Comments
 (0)