Inductive truth := Yes | No | Maybe. Definition not (t : truth) := match t with | Yes => No | No => Yes | Maybe => Maybe end. Definition and (t1 t2 : truth) := match (t1,t2) with | (Yes,Yes) => Yes | (No,No) => No | _ => Maybe end. Definition or (t1 t2 : truth) := match (t1,t2) with | (Yes,_) => Yes | (_,Yes) => Yes | (No,No) => No | _ => Maybe end. Lemma and_comm : forall (t1 t2 t3 : truth), and t1 (and t2 t3) = and (and t1 t2) t3. Proof. intros. destruct t1; destruct t2; destruct t3; simpl; try tauto. Qed. Lemma or_dist_r : forall (t1 t2 t3 : truth), and t1 (or t2 t3) = or (and t1 t2) (and t1 t3). Proof. intros. destruct t1; destruct t2; destruct t3; simpl; try tauto. Qed. Lemma or_dist_l : forall (t1 t2 t3 : truth), and (or t1 t2) t3 = or (and t1 t3) (and t2 t3). Proof. intros. destruct t1; destruct t2; destruct t3; simpl; try tauto. Qed.