equal
deleted
inserted
replaced
10 lemma list_eq_equivp: |
10 lemma list_eq_equivp: |
11 shows "equivp list_eq" |
11 shows "equivp list_eq" |
12 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
12 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
13 by auto |
13 by auto |
14 |
14 |
15 quotient fset = "'a list" / "list_eq" |
15 quotient_type fset = "'a list" / "list_eq" |
16 by (rule list_eq_equivp) |
16 by (rule list_eq_equivp) |
17 |
17 |
18 lemma not_nil_equiv_cons: |
18 lemma not_nil_equiv_cons: |
19 "\<not>[] \<approx> a # A" |
19 "\<not>[] \<approx> a # A" |
20 by auto |
20 by auto |